+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,
+not to Id.
+
+