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 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.
+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,
> 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]`. A predicative proposition cannot be eliminated toward
-`Type[j]` unless it holds no computational content (i.e. it is an inductive type
+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,
+not to Id.
+
+
The standard library and the `include` command
----------------------------------------------
projects / helm.git / blobdiff