Homotopy Type Theory and Univalent Foundations - Mini-Symposium at DMV 2015

Torus
This webpage provides information about the mini-symposium on HoTT and UF that takes place during the convention of the German Mathematical Society (Deutsche Mathematiker-Vereinigung (DMV)) in Hamburg, Germany, in September 2015.

When and where

Thursday 24 Sept (Room W221):
10:30-11:00 Streicher, Various ways of splitting and equality of objects
11:00-11:30 Hofmann, The groupoid interpretation of type theory, a personal retrospective (slides)
11:30-12:00 Gambino, Aspects of univalence
12:00-12:30 Schreiber, Some thoughts on the future of modal homotopy type theory (Notes)
17:45-18:15 Spitters, Cubical sets as a classifying topos
18:15-18:45 v. d. Berg, Weak universes and homotopy exact completion.
Friday 25 Sept (Room W221):
10:30-11:00 Awodey, On the cubical model of HoTT
11:00-11:30 Huber, A Cubical Type Theory
11:30-12:00 Altenkirch, The coherence problem in HoTT
12:00-12:30 Møgelberg, Towards guarded recursion in HoTT
14:00-14:30 v. Glehn, Models of homotopy type theory
14:30-15: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 30-minute slots: presentation, discussion and a brief break for switching speakers.

Organizers

Confirmed speakers

  1. Thorsten Altenkirch (U Nottingham)
  2. Steve Awodey (Carnegie Mellon U)
  3. Benno v. d. Berg (U Amsterdam)
  4. Nicola Gambino (U Leeds)
  5. Tamara v. Glehn (U Cambridge)
  6. Martin Hofmann (LMU Munich)
  7. Simon Huber (Chalmers U)
  8. Peter LeFanu Lumsdaine (Stockholm U)
  9. Rasmus Møgelberg (Copenhagen U)
  10. Urs Schreiber (Charles U Prague)
  11. Bas Spitters (U Aarhus)
  12. 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 work-in-progress 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 Identity-elimination rule of Martin-Löf, and the closure of Kan objects under function spaces is ensured constructively by Coquand’s uniformity condition, re-analysed 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 Lumsdaine-Warren 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 well-behaved 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 Martin-Lö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 well-known results about extensional Martin-Lö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 n-dimensional 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 n-dimensional 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 meta-theory, 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 small-ish dependent type theory.  To minimise meta-theoretic assumptions, we use a setoid-based notion of categories with attributes, rather than categories or pre-categories in the sense of HoTT; however, due to the interaction between the set(oid)s of types and the (E-)category of contexts, a HoTT-like 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 1-toposes this seems inconclusive, one finds [3] that internal to infinity-toposes 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 under-explored 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.

DVMLG