-Type is the sort of sets equipped with the Id equality (i.e. an intensional,
-not quotiented set). We will avoid using Leibnitz equality Id,
-thus we will explicitly equip a set with an equality when needed.
-We will call this structure `setoid`. Note that we will
-attach the infix = symbol only to the equality of a setoid,
+Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
+not quotiented set).
+
+We write `Type[i]` to mention a Type in the predicative hierarchy
+of types. To ease the comprehension we will use `Type[0]` for sets,
+and `Type[1]` for classes. The index `i` is just a label: constraints among
+universes are declared by the user. The standard library defines
+
+> Type[0] < Type[1] < Type[2]
+
+<object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
+
+For every `Type[i]` there is a corresponding level of predicative
+propositions `CProp[i]` (the C initial is due to historical reasons, and
+stands for constructive, `PProp` would be more appropriate).
+A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
+with 0 or 1 constructors with propositional arguments, like `Id` and `And`
+but not like `Or`).
+
+The distintion between predicative propositions and predicative data types
+is a peculirity of Matita (for example in CIC as implemented by Coq they are the
+same). The additional restriction of not allowing the elimination of a CProp
+toward a Type makes the theory of Matita minimal in the following sense:
+
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+
+Theorems proved in this setting can be reused in a classical framwork (forcing
+Matita to collapse the hierarchy of constructive propositions). Alternatively,
+one can decide to collapse predicative propositions and datatypes recovering the
+Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to
+provide a witness for a Σ).
+
+Formalization choices
+---------------------
+
+We will avoid using `Id` (Leibniz equality),
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,