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"/>
+<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
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 formaliztion uses `Id`.
+The current version of the formalization uses `Id`.
The standard library and the `include` command
----------------------------------------------
That, up to rewriting with the equation defining `x`, is what we mean.
Since we decided to use `Id` the rewriting always work (the elimination
-prnciple for `Id` is Leibnitz's equality, that is quantified over
+principle for `Id` is Leibnitz's equality, that is quantified over
the context.
The problem that arises if we decide to make `S` a setoid is that
-`V` has to be extensional w.r.t. the equality of `S` (i.e. the charactestic
+`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic
functional proposition has to quotient its input with a relation bigger
than the one of `S`.
D[retr-3]
To use the equation defining `b` we have to eliminate `H`. Unfolding
definitions in `x` tell us there is still something to do. The `nrewrite`
-tactic is a shorcut for the elimination principle of the equlity.
+tactic is a shortcut for the elimination principle of the equality.
It accepts an additional argument `<` or `>` to rewrite left-to-right
or right-to-left.
D*)
-
-alias symbol "exists" (instance 1) = "exists".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
+alias symbol "covers" (instance 3) = "new covers set".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
#A; #U; #a; (** screenshot "n-cov-inf-1". *)