[Hott meeting at DMV 2015](https://sites.google.com/site/dmv2015hott/) * Streicher, Various ways of splitting and equality of objects * Hofmann, The groupoid interpretation of type theory, a personal retrospective ([[HofmannDMV.pdf:file]]) * Gambino, Aspects of univalence ([[GambinoDMV.pdf:file]]) * Schreiber, Some thoughts on the future of modal homotopy type theory ([Notes](https://dl.dropboxusercontent.com/u/12630719/SchreiberDMV2015b.pdf)) * 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.