next day
all days

View: session overviewtalk overviewside by side with other conferences

09:30-10:30 Session 24A
Location: Blavatnik LT1
Axiomatizing Cubical Sets Models of Univalent Foundations

ABSTRACT. The constructive model of Homotopy Type Theory introduced by Cohen-Coquand-Huber-Mörtberg in 2015 (building on the work of Bezem-Coquand-Huber in 2013) uses a particular presheaf topos of cubical sets. It is arguably one of the most significant contributions to constructive mathematics since Martin-Löf's work in the 1970s. Since its introduction, much effort has been expended to analyse, simplify and generalize what makes this model of the univalence axiom tick, using a variety of techniques. In this talk I will describe an axiomatic approach -- the isolation of a few elementary axioms about an interval and a universe of fillable shapes that allow a univalent universe to be constructed. Not all the axioms are visible in the original work; and the axioms can be satisfied in toposes other than the original presheaf topos of cubical sets. The axioms and constructions can almost be expressed in Extensional Martin-Löf Type Theory, except that the global nature of some of them leads to the use of a modal extension of that language. This is joint work with Ian Orton, Dan Licata and Bas Spitters.

10:30-11:00Coffee Break
11:00-12:30 Session 26F
Location: Blavatnik LT1
Internalizing Presheaf Semantics: Charting the Design Space
SPEAKER: Andreas Nuyts

ABSTRACT. Presheaf semantics are an excellent tool for modelling relational preservation properties of (dependent) type theory. They have been applied to parametricity (which is about preservation of relations), univalent type theory (which is about preservation of equivalences), and directed type theory (which is about preservation of morphisms). Of course after going through the endeavour of constructing a presheaf model of type theory, we want type-theoretic profit, i.e. we want internal operations that allow us to write cheap proofs of the 'free' theorems that follow from the preservation property concerned. There is currently no general theory of how we should craft such operations. Cohen et al. introduced the final type extension operation Glue, using which one can prove the univalence axiom and hence also the 'free' equivalence theorems it entails. In previous work with Vezzosi, we showed that Glue and its dual, the initial type extension operation Weld, can be used to internalize parametricity to some extent. Earlier, Bernardy, Coquand and Moulin had introduced completely different 'boundary-filling' operations to internalize parametricity. Each of these operations has to our knowledge only been used in concrete models and hence their expressivity has not been compared. We have done some work to fill the hiatus: we consider and compare the various operators in more general presheaf categories. In this first step, we do not consider fibrancy requirements.

Cubical Assemblies and the Independence of the Propositional Resizing Axiom
Dependent Right Adjoint Types
SPEAKER: Bas Spitters
12:30-14:00Lunch Break
15:00-15:30 Session 30C
Location: Blavatnik LT1
Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
15:30-16:00Coffee Break
16:00-18:00 Session 31F
Location: Blavatnik LT1
Univalent Foundations and the Constructive View of Theories
Algebraic models of dependent type theory
First-order homotopical logic and Grothendieck fibrations
19:45-22:00 Workshops dinner at Balliol College

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).

Location: Balliol College