# Homotopy Type Theory type theory > history (Rev #6)

## 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?

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)