Motivation, background. Kolmogorov's and Heyting's explanations of
the logical constants.
An overview of the polymorhic type theory. This is an obsolete
theory which is a historical stepping stone towards the
monomorphic theory. Syntax: the theory of expressions with their
arities.
Semantics of the different judgement forms. Structure of the
formal system.
The cartesian product between two sets and the disjoint union of a
family of sets. Different reading of the rules. Enumeration sets.
Natural numbers. The cartesian product of a family of sets and its
special cases (the for all quantifier, the set of functions,
implication).
Propositional equality.
A brief overview of the monomorphic theory. Types and
objects. Definitions. How to represent a proof. How to build a proof.
The compiler example.
Universes and wellorderings. How to express different inductive
sets using wellorderings and the problem with intensional
equality.
Peano's fourth axiom.