+The tutorial spends a considerable amount of effort in defining
+notations that resemble the ones used in the original paper. We believe
+this is a important part of every formalization, not only from the aesthetic
+point of view, but also from the practical point of view. Being
+consistent allows to follow the paper in a pedantic way, and hopefully
+to make the formalization (at least the definitions and proved
+statements) readable to the author of the paper.
+
+Orienteering
+------------
+
+The graphical interface of Matita is composed of three windows:
+the script window, on the left, is where you type; the sequent
+window on the top right is where the system shows you the ongoing proof;
+the error window, on the bottom right, is where the system complains.
+On the top of the script window five buttons drive the processing of
+the proof script. From left to right the requesting the system to:
+
+- go back to the beginning of the script
+- go back one step
+- go to the current cursor position
+- advance one step
+- advance to the end of the script
+
+When the system processes a command, it locks the part of the script
+corresponding to the command, such that you cannot edit it anymore
+(without to go back). Locked parts are coloured in blue.
+
+The sequent window is hyper textual, i.e. you can click on symbols
+to jump to their definition, or switch between different notation
+for the same expression (for example, equality has two notations,
+one of them makes the type of the arguments explicit).
+
+Everywhere in the script you can use the `ncheck (term).` command to
+ask for the type a given term. If you that in the middle of a proof,
+the term is assumed to live in the current proof context (i.e. can use
+variables introduced so far).
+
+To ease the typing of mathematical symbols, the script window
+implements two unusual input facilities:
+
+- some TeX symbols can be typed using their TeX names, and are
+ automatically converted to UTF-8 characters. For a list of
+ the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
+ Moreover some ASCII-art is understood as well, like `=>` and `->`
+ to mean double or single arrows.
+ Here we recall some of these "shortcuts":
+
+ - ∀ can be typed with `\Forall`
+ - λ can be typed with `\lambda`
+ - ≝ can be typed with `\def` or `:=`
+ - → can be typed with `\to` or `->`
+
+- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
+ The user can cycle between variants typing one of them and then
+ pressing ALT-L. Note that also letters do have variants, for
+ example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
+ Variants are listed in the aforementioned TeX/UTF-8 table.
+
+Pressing `F1` opens the Matita manual.
+
+CIC (as implemented in Matita) in a nutshell
+--------------------------------------------
+
+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impedicative sort
+Prop and a predicative sort Type. The environment can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical
+analysis (recursive call on structurally smaller subterms). Co-recursive
+functions can be defined as well, and must satisfy a dual condition, that is
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment that combined with the definable total
+structural recursive functions allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly types
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
+
+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 Leibnitz equality Id,
+thus we will explicitly equip a set with an equality when needed.
+We will call this structure `setoid`. Note that we will
+attach the infix = symbol only to the equality of a setoid,
+not to Id.
+
+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.
+
+For every Type[i] there is a corresponding level of predicative
+propositions CProp[i].