Idea

A type theory is a formal system in which every term has a ‘type’, and operations in the system are restricted to acting on specific types.

A number of type theories have been used or proposed for doing homotopy type theory.

List of types in HoTT

Typically types come with four sets of inference rules. Rules allow one to conclude one set of judgements from others. A collection of judgements is typically called a context.

• function type $A \to B$
• pi type? $\prod_{a:A}B$
• universe $\mathcal{U}$
• product type? $A \times B$
• sigma type? $\sum_{a:A}B$
• zero type?
• unit type?

List of axioms in HoTT

• univalence
• function extensionality
• propositional resizing?

See axioms

Old page

List of examples

This page lists some of the type theories and variations that have been used or proposed for doing homotopy type theory.

• The system presented in the HoTT book, chapter 1 and appendix A.
• Martin-Löf Intensional Type Theory: the original.
• The Calculus Of Constructions?: the basis of the Coq proof assistant.
• Agda: based on Martin-Löf type theory, extended by a flexible scheme for specifying inductive definitions.
• Homotopy Type System: a proposal by Vladimir Voevodsky.
• Two-level type theory?
• cubical type theory? (which has various forms)

See also

‘Type theory’ on the nLab wiki.