type theories (Rev #3, changes)

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

This page~~ is~~ lists~~ a~~ some~~ list~~ of the type theories and~~ their~~ variations that have been used or proposed for doing homotopy type~~ theory~~ theory.~~ /~~~~ univalent~~~~ foundations.~~

- 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
~~Coq.~~the Coq proof assistant. ~~The type theory of~~Agda :~~apparently~~based~~has~~on~~no~~Martin-Löf~~formal~~type~~definition~~theory,~~other~~extended~~than~~by~~the~~a~~Agda~~flexible~~source~~scheme~~code.~~for specifying inductive definitions.~~Vladimir Voevodsky~~~~’s~~Homotopy Type System: work in progress based on a proposal by Vladimir Voevodsky.

Revision on May 9, 2014 at 00:41:23 by Steve Awodey. See the history of this page for a list of all contributions to it.