Homotopy Type Theory DMV2015 > history (Rev #2)

Hott meeting at DMV 2015

• Streicher, Various ways of splitting and equality of objects

• Hofmann, The groupoid interpretation of type theory, a personal retrospective (Hofmann's slides from DMV2015)

• Gambino, Aspects of univalence (Gambino)

• Schreiber, Some thoughts on the future of modal homotopy type theory (Notes)

• Spitters, Cubical sets as a classifying topos

• v. d. Berg, Weak universes and homotopy exact completion.

• Awodey, On the cubical model of HoTT

• Huber, A Cubical Type Theory

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