Homotopy Type Theory DMV2015 > history (Rev #14)

Homotopy Type Theory and Univalent Foundations at DMV 2015

The abstracts are available on the site above.

• Thomas Streicher, Various ways of splitting and equality of objects (slides)

• Martin Hofmann, The groupoid interpretation of type theory, a personal retrospective (slides)

• Nicola Gambino, Aspects of univalence (slides)

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

• Bas Spitters, Cubical sets as a classifying topos (slides)

• Benno van den Berg, Weak universes and homotopy exact completion

• Steve Awodey, On the cubical model of HoTT (slides)

• Simon Huber, A Cubical Type Theory (slides)

• Thorsten Altenkirch, The coherence problem in HoTT (slides)

• Rasmus Møgelberg, Towards guarded recursion in HoTT (slides)

• Tamara von Glehn, Models of homotopy type theory

• Peter LeFanu Lumsdaine, Formalising the categorical semantics of type theory, in type theory (slides)