Homotopy Type Theory type theory > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

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.

~~See also~~

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: work in progress based on a proposal by Vladimir Voevodsky.