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

Showing changes from revision #2 to #3: Added | Removed | Changed

Hott meeting at DMV 2015

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