> explicit solution for the conditions for an
> inductive generation of formal topologies
-by S.Berardi and S. Valentini.
+by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
Orientering
-----------
Defining Axiom set
------------------
-records, ...
+records, projections, types of projections..
DOCEND*)
nrecord Ax : Type[1] ≝ {
- S:> setoid;
- I: S → Type[0];
- C: ∀a:S. I a → Ω ^ S
+ S :> setoid;
+ I : S → Type[0];
+ C : ∀a:S. I a → Ω ^ S
}.
(*DOCBEGIN
-TODO: coercion S.
+Note that the field `S` was declared with `:>` instead of a simple `:`.
+This declares the `S` projection to be a coercion. A coercion is
+a function case the system automatically inserts when it is needed.
+In that case, the projection `S` has type `Ax → setoid`, and whenever
+the expected type of a term is `setoid` while its type is `Ax`, the
+system inserts the coercion around it, to make the whole term well types.
+
+When formalizing an algebraic structure, declaring the carrier as a
+coercion is a common practice, since it allows to write statements like
+
+ ∀G:Group.∀x:G.x * x^-1 = 1
+
+The quantification over `x` of type `G` is illtyped, since `G` is a term
+(of type `Group`) and thus not a type. Since the carrier projection
+`carr` of `G` is a coercion, that maps a `Group` into the type of
+its elements, the system automatically inserts `carr` around `G`,
+obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
+when it displays a term.
+
+In this particular case, the coercion `S` allows to write
+
+ ∀A:Ax.∀a:A.…
+
+Since `A` is not a type, but it can be turned into a `setoid` by `S`
+and a `setoid` can be turned into a type by its `carr` projection, the
+composed coercion `carr ∘ S` is silently inserted.
+
+Implicit arguments
+------------------
Something that is not still satisfactory, in that the dependent type
of `I` and `C` are abstracted over the Axiom set. To obtain the
One would like to write `I a` and not `I A a` under a context where
`A` is an axiom set and `a` has type `S A` (or thanks to the coercion
-mecanism simply `A`). Matita performs type inference, thus writing
-`I ? a` is enough, since the second argument of `I` is typed by the
+mecanism simply `A`). In Matita, a question mark represents an implicit
+argument, i.e. a missing piece of information the system is asked to
+infer. Matita performs some sort of type inference, thus writing
+`I ? a` is enough: since the second argument of `I` is typed by the
first one, the first one can be inferred just computing the type of `a`.
DOCEND*)
(*DOCBEGIN
-This is still not completely satisfactory, and to fix this minor issue
-we have to introduce the notational support built in Matita.
+This is still not completely satisfactory, since you have always type
+`?`; to fix this minor issue we have to introduce the notational
+support built in Matita.
Notation for I and C
--------------------
-Matita is quipped qith a quite complex notational support,
+Matita is quipped with a quite complex notational support,
allowing the user to define and use mathematical notations
([From Notation to Semantics: There and Back Again][1]).
Since notations are usually ambiguous (e.g. the frequent overloading of
symbols) Matita distinguishes between the term level, the
-content level, and the presentation level.
+content level, and the presentation level, allowing multiple
+mappings between the contenet and the term level.
The mapping between the presentation level (i.e. what is typed on the
keyboard and what is displayed in the sequent window) and the content
have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
To obtain the `𝐈` is enough to type `I` and then cycle between its
-similar symbols with ALT-L. The same for `𝐂`. Notationa cannot use
+similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
regular letters or the round parentheses, thus their variants (like the
bold ones) have to be used.
projects / helm.git / commitdiff