[Homotopy Type Theory and Univalent Foundations at DMV 2015](https://sites.google.com/site/dmv2015hott/) The abstracts are available on the site above. * [[nLab:Thomas Streicher]], _Various ways of splitting and equality of objects_ ([slides](http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/SpFi2015.pdf)) * [[nLab:Martin Hofmann]], _The groupoid interpretation of type theory, a personal retrospective_ ([[HofmannDMV.pdf|slides:file]]) * [[nLab:Nicola Gambino]], _Aspects of univalence_ ([[GambinoDMV.pdf|slides:file]]) * [[nLab:Urs Schreiber]], _Some thoughts on the future of modal homotopy type theory_ ([Notes](https://dl.dropboxusercontent.com/u/12630719/SchreiberDMV2015b.pdf)) * [[nLab:Bas Spitters]], _Cubical sets as a classifying topos_ ([[SpittersDMV.pdf|slides:file]]) * [[nLab:Benno van den Berg]], _Weak universes and homotopy exact completion_ * [[nLab:Steve Awodey]], _On the cubical model of HoTT_ ([[AwodeyDMVrev.pdf|slides:file]]) * [[nLab:Simon Huber]], _A Cubical Type Theory_ ([slides](http://www.cse.chalmers.se/~simonhu/slides/hamburg2015.pdf)) * [[nLab:Thorsten Altenkirch]], _The coherence problem in HoTT_ ([[Altenkirch.pdf|slides:file]]) * [[nLab:Rasmus Møgelberg]], _Towards guarded recursion in HoTT_ * [[nLab:Tamara von Glehn]], _Models of homotopy type theory_ * [[nLab:Peter LeFanu Lumsdaine]], _Formalising the categorical semantics of type theory, in type theory_ ([slides](http://peterlefanulumsdaine.com/research/Lumsdaine-2015-DMV-Hamburg-slides-Formalising-semantics-of-DTT-in-DTT.pdf))