+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impedicative sort
+Prop and a predicative sort Type. The environment can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical
+analysis (recursive call on structurally smaller subterms). Co-recursive
+functions can be defined as well, and must satisfy a dual condition, that is
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment that combined with the definable total
+structural recursive functions allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly types
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).