Homotopy Type Theory type theories > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | ~~Removed~~ | ~~Chan~~ged

~~This~~ See ~~page~~ ~~lists~~ ~~some~~ of ~~the~~ ~~type~~ ~~theories~~ ~~and~~ ~~variations~~ ~~that~~ ~~have~~ ~~been~~ ~~used~~ or ~~proposed~~ ~~for~~ ~~doing~~ ~~homotopy~~ ~~type~~ ~~theory.~~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.

Revision on September 3, 2018 at 10:03:38 by Ali Caglayan. See the history of this page for a list of all contributions to it.