Foundations and Applications of Univalent Mathematics

Supported by the Junior Researcher Fund, LMUexcellent

18-20 December 2019, Herrsching (near Munich), Germany

This is a project kickoff workshop.

It focuses on both the foundation of univalent mathematics and the applications of the univalent innovations.

Invited speakers

Preliminary programme

Wednesday 18.12 Thursday 19.12 Friday 20.12
09:30 - 10:15 Escardó Streicher Coquand
10:15 - 11:00 Kraus Buchholtz van den Berg
11:00 - 11:30 Coffee Coffee Coffee
11:30 - 12:15 Altenkirch Awodey Bauer
12:15 - 14:30 Lunch Lunch Lunch
14:30 - 15:15 Ahrens Petrakis Coffee
15:15 - 16:00 Vezzosi Isaev Discussion
16:00 - 16:30 Coffee Coffee
16:30 - 17:15 North Nordvall Forsberg
17:15 - 18:00 Dybjer Spitters
Benedikt Ahrens: A Higher Structure Identity Principle
j.w.w. Paige North, Mike Shulman, and Dimitris Tsementzis

The Structure Identity Principle (SIP) is an informal principle asserting that reasoning about mathematical structures is invariant under isomorphism of such structures. In univalent foundations, the SIP can be formally stated and proved for a variety of mathematical structures. This means that any statement about such structures that can be expressed in univalent foundations is invariant under isomorphism, or, put differently, that only structural properties of such structures can be stated in univalent foundations.

The SIP as stated in, e.g., [1] and [2], only applies to structures that naturally form the objects of a 1-category. In this talk, we discuss a Higher Structure Identity Principle in univalent foundations, for structures that naturally form a higher category (e.g., categories themselves).

[1] Thierry Coquand, Nils Anders Danielsson, "Isomorphism is equality", https://doi.org/10.1016/j.indag.2013.09.002
[2] Homotopy Type Theory: Univalent Foundations of Mathematics, https://homotopytypetheory.org/book/, Section 9.8 "The structure identity principle"
Steve Awodey: Composition, Filling, and the Fibrancy of the Universe
j.w.w. Thierry Coquand

This talk outlines a new construction of the universe of Kan fibrations in cubical sets, and a new proof that it is fibrant. The constructions and proofs are entirely algebraic.
Peter Dybjer: Categories with Families: Unityped, Simply Typed, and Dependently Typed
j.w.w. Simon Castellan (Imperial College, London) and Pierre Clairambault (ENS Lyon)

We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with families (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. We also discuss how these theorems can be formalised as weak equivalence between types in univalent type theory.
Nicolai Kraus: Coherence via Well-founded Relations
j.w.w. Jakob von Raumer

Set-quotients come with the built-in restriction of only eliminating into sets. If higher types are involved, this becomes problematic; sample cases include [approximations to] open questions around "HoTT eating itself", free higher groups, and pushouts of sets. The coherence data needed to tackle these problems is based on zig-zags and cycles, which are hard to work with. Fortunately, the relations relevant in these situations are often well-founded, and I show how combinatorial arguments can help to manage the coherences.
Paige Randall North: Two-sided Weak Factorization Systems for Directed Type Theory
In this talk, I'll describe intended semantics for directed type theory. We generalize the two-sided fibrations of Street to obtain a notion of two-sided weak factorization systems: structure on a category which consists of two compatible weak factorization systems. These correspond to a notion of directed path object. The long-term goal is to use the behavior of these directed path objects to reverse-engineer a directed identity type.
Bas Spitters: Synthetic topology in Homotopy Type Theory for probabilistic programming
j.w.w. Martin Bidlingmaier (Aarhus) and Florian Faissole (INRIA)

The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. Continuous distributions (e.g. over the reals) cannot be treated this way, as not all subsets are measurable. We propose the use of synthetic topology to model continuous distributions while staying close to ALEA's approach. This allows us to model the apWhile language used in easycrypt to model differential privacy. We study the initial sigma-frame and the corresponding induced topology on arbitrary sets. We define valuations and lower integrals on sets that takes into account these intrinsic topologies, and we prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed. By interpreting our synthetic results in the K2-realizability topos, we recover the valuations on topological domains used as the semantics for the augurv2 probabilistic language, which has been used for machine learning.
Thomas Streicher: Simplicial Sets within Cubical Sets
j.w.w. Jonathan Weinberger

We discuss a sequence of three adjoints between simplicial and cubical sets and show (borrowing results from Ch. Sattler) that they are both Quillen adjunctions. Alas, we don't know whether one of them at least is a Quillen equivalence. But we explicitate to which combinatorial property this would amount to.
Benno van den Berg: Homotopy Type Theory with Explicit Conversions
abstractMuch recent work in type theory, and in homotopy type theory (HoTT) especially, concerns equality. Martin-Löf's Type Theory has two kinds of equality: judgmental (also: definitional) and propositional. HoTT starts from a novel interpretation of propositional equality as a space of paths and has lead to a much better understanding of propositional equality. In this talk I will argue that one thing that recent work in HoTT has shown, is that it is feasible to completely eliminate judgmental equality in favour of propositional equality and state all computation rule as propositional equalities. In this talk I wish to present such a purely propositional type theory, reminiscent of "A Logical Framework with Explicit Conversions" by Geuvers and Wiedijk, and discuss its properties (many in the form of conjectures).
Andrea Vezzosi: Partial Univalence in n-truncated Type Theory
j.w.w. Christian Sattler

It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions.

A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in HoTT. This universe has a path constructor for simultaneous "partial" univalent completion, restricted to h-propositions.

More generally, we show that univalence restricted to (n-1)-types is consistent with the assumption that all types are n-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.

Practical information

Venue

Haus der Bayerischen Landwirtschaft Herrsching
Rieder Str. 70
82211 Herrsching am Ammersee

Accommodation

Full-board accommodation at HdBL Herrsching (few rooms available):
  • The default arrival time is the afternoon/evening of Tuesday 17.12.2019, and
  • the departure time the afternoon of Friday 20.12.2019.
There are also other options of accommodation in Herrsching am Ammersee and downtwon Munich.

Getting to the venue

There are frequent suburban trains (line S8) from the Munich airport and downtown Munich to Herrsching (last stop). From the train station in Herrsching, it takes about 30 minutes to walk to the venue, or you can take Bus 921 to Herrsching-Lochschwab (2 stops). Please see the venue's website for directions.

Registration

Registration is now closed.

Please note that participation is restricted to registered participants.