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

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

Revision on September 4, 2018 at 04:43:48 by
Mike Shulman.
See the history of this page for a list of all contributions to it.