+Since we are going to formalize constructive and predicative mathematics
+in an intensional type theory like CIC, we try to establish some terminology.
+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]
+
+Matita implements a variant of CIC in which constructive and predicative proposition
+are distinguished from predicative data types.
+
+<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).
+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 distinction between predicative propositions and predicative data types
+is a peculiarity 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="600px"/>
+
+Theorems proved in CIC as implemented in Matita can be reused in a classical
+and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
+constructive propositions and assuming the excluded middle on them).
+Alternatively, one can decide to collapse predicative propositions and
+predicative data types recovering the Axiom of Choice in the sense of Martin Löf
+(i.e. ∃ really holds a witness and can be eliminated to inhabit a type).
+
+This implementation of CIC is the result of the collaboration with Maietti M.,
+Sambin G. and Valentini S. of the University of Padua.
+
+Formalization choices
+---------------------
+
+There are many different ways of formalizing the same piece of mathematics
+in CIC, depending on what our interests are. There is usually a trade-off
+between the possibility of reuse the formalization we did and its complexity.
+
+In this work, our decisions mainly regarded the following two areas
+
+- Axiom of Choice: controlled use or not
+- Equality: Id or not
+
+### Axiom of Choice
+
+In this paper it is clear that the author is interested in using the Axiom
+of Choice, thus choosing to identify ∃ and Σ (i.e. working in the
+leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision
+(that is, the author of the paper would not complain we formalized something
+different from what he had in mind).
+
+Anyway, we may benefit from the minimality of CIC as implemented in Matita,
+"asking" the type system to ensure we do no use the Axiom of Choice elsewhere
+in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
+very beginning, the system will not complain if we use the Axiom of Choice at all.
+Moreover, the elimination of an inductive type (like ∃) is a so common operation
+that the syntax chosen for the elimination command is very compact and non
+informative, hard to spot for a human being
+(in fact it is just two characters long!).
+
+We decided to formalize the whole paper without identifying
+CProp and Type and assuming the Axiom of Choice as a real axiom
+(i.e. a black hole with no computational content, a function with no body).
+
+It is clear that this approach give us full control on when/where we really use
+the Axiom of Choice. But, what are we loosing? What happens to the computational
+content of the proofs if the Axiom of Choice gives no content back?
+
+It really
+depends on when we actually look at the computational content of the proof and
+we "run" that program. We can extract the content and run it before or after
+informing the system that our propositions are actually code (i.e. identifying
+∃ and Σ). If we run the program before, as soon as the computation reaches the
+Axiom of Choice it stops, giving no output. If we tell the system that CProp and
+Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection)
+and the extracted code would compute an output.
+
+Note that the computational
+content is there even if the Axiom of Choice is an axiom, the difference is
+just that we cannot use it (the typing rules inhibit the elimination of the
+existential). This is possible only thanks to the minimality of CIC as implemented
+in Matita.
+
+### Equality
+
+What we have to decide here is which models we admit. The paper does not
+mention quotiented sets, thus using an intensional equality is enough
+to capture the intended content of the paper. Nevertheless, the formalization
+cannot be reused in a concrete example where the (families of) sets
+that will build the axiom set are quotiented.
+
+Matita gives support for setoid rewriting under a context built with
+non dependent morphisms. As we will detail later, if we assume a generic
+equality over the carrier of our axiom set, a non trivial inductive
+construction over the ordinals has to be proved to respect extensionality
+(i.e. if the input is an extensional set, also the output is).
+The proof requires to rewrite under the context formed by the family of sets
+`I` and `D`, that have a dependent type. Declaring them as dependently typed
+morphisms is possible, but Matita does not provide an adequate support for them,
+and would thus need more effort than formalizing the whole paper.
+
+Anyway, in a preliminary attempt of formalization, we tried the setoid approach,
+reaching the end of the formalization, but we had to assume the proof
+of the extensionality of the `U_x` construction (while there is no
+need to assume the same property for `F_x`!).
+
+The current version of the formalization uses `Id`.