This webpage provides information about the minisymposium on HoTT and UF that takes place during the convention of the German Mathematical Society (Deutsche MathematikerVereinigung (DMV)) in Hamburg, Germany, in September 2015.
Thursday 24 Sept ( Room W221):
10:3011:00 Streicher, Various ways of splitting and equality of objects
11:0011:30 Hofmann, The groupoid interpretation of type theory, a personal retrospective (slides)
11:3012:00 Gambino, Aspects of univalence
12:0012:30 Schreiber, Some thoughts on the future of modal homotopy type theory ( Notes)
17:4518:15 Spitters, Cubical sets as a classifying topos
18:1518:45 v. d. Berg, Weak universes and homotopy exact completion.
Friday 25 Sept ( Room W221):
10:3011:00 Awodey, On the cubical model of HoTT
11:0011:30 Huber,
A Cubical Type Theory
11:3012:00 Altenkirch, The coherence problem in HoTT
12:0012:30 Møgelberg, Towards guarded recursion in HoTT
14:0014:30 v. Glehn, Models of homotopy type theory
14:3015:00 Lumsdaine, Formalising the categorical semantics of type theory, in type theory.
Please note: early registration closes on 15 June.
There will be no black board available.
The lectures are in 30minute
slots: presentation,
discussion and a brief break for switching speakers.
Organizers
Confirmed speakers
 Thorsten Altenkirch (U Nottingham)
 Steve Awodey (Carnegie Mellon U)
 Benno v. d. Berg (U Amsterdam)
 Nicola Gambino (U Leeds)
 Tamara v. Glehn (U Cambridge)
 Martin Hofmann (LMU Munich)
 Simon Huber (Chalmers U)
 Peter LeFanu Lumsdaine (Stockholm U)
 Rasmus Møgelberg (Copenhagen U)
 Urs Schreiber (Charles U Prague)
 Bas Spitters (U Aarhus)
 Thomas Streicher (U Darmstadt)
Titles and abstracts
 Thorsten Altenkirch: The coherence problem in HoTT
Abstract: All attempts to internalise semisimplicial types in HoTT have failed, due to a coherence problem: how do we make precise the notion of an omega functor? This is not the only instance of such a problem. We suggest a two level system, which introduces pre types with a notion of strict equality and a universe of types with an extensional, univalent equality. This is inspired by Voevodsky¹s HTS but unlike HTS our approach is an extension of intensional type theory and can be easily formalised within existing systems like Agda. Our approach works for type valued pre shaves over a Reedy category. This relies on the assumption that the basic types like natural numbers agree with their pre type,
 Steve Awodey: On the cubical model of HoTT
Abstract: In this workinprogress talk, I will analyse the cubical model of homotopy type theory of Coquand et al. in functorial terms, making a few adjustments along the way. The basic category of cubical sets used is presheaves on the free cartesian category on a bipointed object, i.e. the Lawvere theory of bipointed objects. The presheaf category is the classifying topos for strictly bipointed objects. The Kan extension property familiar from algebraic topology is shown to be exactly what is required to model the Identityelimination rule of MartinLöf, and the closure of Kan objects under function spaces is ensured constructively by Coquand’s uniformity condition, reanalysed as the existence of a certain natural transformation making natural choices of Kan fillers. A universe of Kan objects is given in the style of the recent “natural models” construction, based on ideas of LumsdaineWarren and Voevodsky
 Benno v. d. Berg: Weak universes and homotopy exact completion.
Abstract: In this talk I will discuss weak universes, with any small type only being weakly equivalent to something inside the universe. The motivation is that it turns out to be much easier to construct models of homotopy type theory with weak univalent universes and that such weak universes are just as wellbehaved as ordinary universes. For example, they also lead to models of CZF: to give a nice categorical proof of this fact we introduce a new categorical construction which we call a "homotopy exact completion". This is ongoing joint work with Ieke Moerdijk.
 Nicola Gambino: Aspects of univalence
Abstract: I will review and discuss some aspects of Voevodsky’s univalence axiom. First, I will illustrate how recent work of Cisinski provides a streamlined proof of the validity of the univalence axiom in the simplicial model. Secondly, I will describe how, in analogy with the notion of a univalent fibration, it is possible to define a notion of univalent dependent type, giving some examples.
 Tamara von Glehn: Models of homotopy type theory
Abstract: In this talk I will consider various constructions of categorical models of dependent type theory, and look at how the fibrations involved interact with the structure required for identity types and enrichment.
 Martin Hofmann: The groupoid interpretation of type theory, a personal retrospective
Abstract: Back in 1994 Thomas Streicher and myself discovered the groupoid interpretation of MartinLöf's type theory which is now seen as a precursor of Homotopy Type Theory and in fact anticipated some simple cases of important ideas of Homotopy Type Theory, notably a special case of the univalence axiom. I will explain how and why we found the groupoid interpretation, our motivations and results. I will also present some less wellknown results about extensional MartinLöf type theory and speculate how this might relate to homotopy type theory.
 Simon Huber: A Cubical Type Theory
Abstract: We present a type theory in which the user can directly manipulate ndimensional cubes (points, lines, squares, cubes, etc.) based on a model of type theory in cubical sets with connections. The identity type is defined as a type of paths and all properties of intensional equality are provable, with the usual definitional equalities. The fact that the user can directly manipulate ndimensional cubes enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, the system also supports transforming any isomorphism into an equality and some higher inductive types like the circle and suspensions. This is joint work with Cyril Cohen, Thierry Coquand, and Anders Mörtberg.
 Peter LeFanu Lumsdaine: Formalising the categorical semantics of type theory, in type theory
Abstract: If we take HoTT (or any system) seriously as a general foundation for mathematics, then we should be willing and able in principle to do all our mathematics within it. This includes setting up the basic proof theory and model theory of the system itself, just as one can for classical foundations. However, existing developments of the general semantics of type theory rely significantly on having a somewhat extensional metatheory, with at least uniqueness of identity proofs.
I will report on work in progress with Håkon Gylterud and Erik Palmgren: a formalisation, in Coq, of the basic algebraic semantics of dependent type theory. Specifically, we aim to show the initiality of the syntactic category with attributes, for a smallish dependent type theory. To minimise metatheoretic assumptions, we use a setoidbased notion of categories with attributes, rather than categories or precategories in the sense of HoTT; however, due to the interaction between the set(oid)s of types and the (E)category of contexts, a HoTTlike worldview inevitably pervades the work.
A related question is whether Homotopy Type Theory can eat itself — that is, whether one can construct in HoTT an interpretation function from some small fragment of its syntax into the actual universe of types. This has proven difficult, perhaps surprisingly so. The present project does not attempt to do this, but it perhaps sheds some light on the difficulties that arise.
 Rasmus Ejlers Møgelberg: Towards guarded recursion in HoTT
Abstract: Guarded recursion is a form of recursion where the recursion
variable is only allowed to appear guarded by a time step. The notion of
time step is encoded in type theory by a modal type operator. Guarded
recursion allows one to solve guarded variants
of otherwise unsolvable type equations, and these have proved useful
for modelling programming languages with advanced features inside type
theory. Guarded recursion can also be used for constructing guarded
variants of coinductive types, such as streams,
and these can be used when constructing and reasoning about elements of
coinductive types. In particular they can be used to encode the notion
of productivity in types.
In the talk I will outline the use of guarded recursion in type
theory and show how guarded recursion can be proved consistent with the
univalence principles by constructing a presheaf model.
 Urs Schreiber: Some thoughts on the future of modal homotopy type theory
Abstract: In 1991 Lawvere suggested a) that the future of category theory revolves around toposes equippped with an adjoint system of idempotent (co)monads [1] and that b) this is formalization of what the ancients had called the "objective logic" [2]. While for 1toposes this seems inconclusive, one finds [3] that internal to infinitytoposes equipped with such adjoint systems much of higher differential geometry and of modern physics has a succinct and useful synthetic formalization. But here the syntax of this internal language is modal homotopy type theory [4]. In this talk I survey the immensely rich semantics and the potential prospects of its full syntactic formalization, in the hope to motivate the type theory community to further look into this fascinating but underexplored aspect of their theory.
[1] http://ncatlab.org/nlab/show/Some+Thoughts+on+the+Future+of+Category+Theory
[2] http://ncatlab.org/nlab/show/Tools+for+the+advancement+of+objective+logic
[3] http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos
[4] http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory
 Bas Spitters, Cubical sets as a classifying topos
Abstract: Coquand’s cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. We show that the underlying cube category is the opposite of the Lawvere theory of De Morgan algebras. The topos of cubical sets itself classifies the theory of ‘free De Morgan algebras’.
We will relate this to Johnstone's topological topos and the nerve construction. This provides us with a topos with an internal ‘interval’. Using this interval we construct a model of type theory following van den Berg and Garner. We are currently investigating the precise relation with Coquand’s model. We do not exclude that the interval can also be used to construct other models.
 Thomas Streicher: Various ways of splitting and equality of objects
Abstract: We recall various ways of splitting fibrations and discuss the role equality of objects plays in there.
Questions?
In case of questions, please contact the organizers.
Support
We are grateful for financial support from the DVMLG.

