Showing changes from revision #2 to #3:
Added | Removed | Changed
Streicher, Various ways of splitting and equality of objectsThomas Streicher, Various ways of splitting and equality of objects
Hofmann, The groupoid interpretation of type theory, a personal retrospective (Martin Hofmann, The groupoid interpretation of type theory, a personal retrospective (Hofmann's slides from DMV2015)
Gambino, Aspects of univalence (Nicola Gambino, Aspects of univalence (Gambino)
Schreiber, Some thoughts on the future of modal homotopy type theory (Urs Schreiber, Some thoughts on the future of modal homotopy type theory (Notes)
Spitters, Cubical sets as a classifying toposBas Spitters, Cubical sets as a classifying topos
v. d. Berg, Weak universes and homotopy exact completion.Benno van den Berg, Weak universes and homotopy exact completion
Awodey, On the cubical model of HoTTSteve Awodey, On the cubical model of HoTT
Huber, A Cubical Type TheorySimon Huber, A Cubical Type Theory
Altenkirch, The coherence problem in HoTTThorsten Altenkirch, The coherence problem in HoTT
Møgelberg, Towards guarded recursion in HoTT
v. Glehn, Models of homotopy type theory
Lumsdaine, Formalising the categorical semantics of type theory, in type theory.Peter Lumsdaine, Formalising the categorical semantics of type theory, in type theory
Revision on September 25, 2015 at 11:11:01 by Urs Schreiber. See the history of this page for a list of all contributions to it.