Foundations and Applications of Univalent Mathematics

This is a kickoff workshop of the project Continuity and Computation in Univalent Mathematics (2CiUM).

2CiUM focuses on both the foundations of univalent mathematics and the applications of the univalent innovations.

Invited speakers

• Benedikt Ahrens (University of Birmingham)
• Thorsten Altenkirch (University of Nottingham)
• Steve Awodey (Carnegie Mellon University)
• Andrej Bauer (University of Ljubljana)
• Ulrik Buchholtz (Technische Universität Darmstadt)
• Thierry Coquand (University of Gothenburg)
• Peter Dybjer (Chalmers University of Technology)
• Martín Escardó (University of Birmingham)
• Valery Isaev (JetBrains Research)
• Nicolai Kraus (University of Birmingham)
• Fredrik Nordvall Forsberg (University of Strathclyde)
• Paige Randall North (Ohio State University)
• Iosif Petrakis (Ludwig-Maximilians-Universität München)
• Bas Spitters (Aarhus University)
• Thomas Streicher (Technische Universität Darmstadt)
• Benno van den Berg (Universiteit van Amsterdam)
• Andrea Vezzosi (IT University of Copenhagen)

Programme

	Wednesday 18.12	Thursday 19.12	Friday 20.12
09:25 - 09:30	Opening
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	Nordvall Forsberg
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	Bauer
17:15 ‐ 18:00	Dybjer	Spitters

Wednesday 18.12.2019

Martín Escardó: Universe Oddities (slides)

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.

Thorsten Altenkirch: On Inductive Types (slides)

Inductive types are a central concept of Type Theory. I will review various incarnations: from simple inductive types, dependent inductive types, induction-induction, quotient inductive types and higher inductive types and their properties. In particular I will discuss the reduction of a class of inductive types to a universal one, e.g. W-types. I will discuss the representation of qotient inductive-inductive types and higher inductive-inductive types via a theory of codes as proposed by Kaposi and Kovac.

Benedikt Ahrens: A Higher Structure Identity Principle (slides)

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"

Andrea Vezzosi: Partial Univalence in n-truncated Type Theory (slides)

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.

Paige Randall North: Two-sided Weak Factorization Systems for Directed Type Theory (slides)

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.

Peter Dybjer: Categories with Families: Unityped, Simply Typed, and Dependently Typed (slides, preprint)

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.

Thursday 19.12.2019

Thomas Streicher: Simplicial Sets within Cubical Sets (slides, preprint)

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.

Ulrik Buchholtz: Higher Homotopy n-groups

j.w.w. Egbert Rijke We've previously explored how convenient it is to use HoTT to reason about higher groups: higher homotopy types with a coherent group structure. One source of examples of these are higher homotopy higher groups: n-truncations of k-fold iterated loop spaces. We continue the development of the theory of k-symmetric n-groups and derive the long exact sequence of homotopy n-groups for a fibration, generalizing the long exact sequence of 1-groups.

Steve Awodey: Composition, Filling, and the Fibrancy of the Universe (slides)

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.

Iosif Petrakis: From Univalent Type Theory to Bishop Set Theory (slides)

In this talk we explain how to translate notions and results from Univalent Type Theory to Bishop's set theory (BST). For the translation of results in Martin-Loef's Type Theory (MLTT) that require the use of transport we use the notion of a set-indexed family of Bishop sets. For results in MLTT that require the axiom of function extensionality we use the canonical equality on the function space. For results in MLTT that require the axiom of univalence, and their formulation does not raise the level of the universe, we use the canonical equality on the class of all Bishop sets. Finally, we sketch how through a proof-relevant formulation of certain equality-conditions on Bishop totalities, some notions and results from the theory of homotopy n-types can be translated in BST.

Valery Isaev: Arend Proof Assistant (slides)

Arend is a proof assistant based on homotopy type theory. It has universes of a given homotopy level, built-in higher inductive types, a convenient pattern matching mechanism for them, path types in the style of cubical type theories, and many other features. We will discuss these features and some of the features that we plan to implement in the future.

Andrej Bauer: A Generic Proof Assistant (slides)

j.w.w. Philipp Haselwarter and Anja Petković I will discuss the implementation of a proof assistant that supports user-definable theories. In order to make it useful, it has to support at least equality checking, even though in general a type theory may have undecidable type-checking. Nevertheless, we can design an equality checking algorithm that works for a class of well-behaved type theories that occur in practice.

Bas Spitters: Synthetic Topology in Homotopy Type Theory for Probabilistic Programming (slides, preprint)

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.

Friday 20.12.2019

Thierry Coquand: Constructive Stacks? (slides)

This talk will explore the notion of stacks (sheaves for type theory) in a constructive metatheory. We first present an abstract notion of descent data, as a special kind of a type theoretic version of an endomorphism of tribes (as introduced by André Joyal). We then show that such a notion induces a left exact modality and a corresponding model of univalent type theory (with HITs). Finally, we explain how to define such a notion given a Grothendieck topology on a small category. Even when the topology is trivial, we get new models of type theory, where equivalence coincides with pointwise equivalence. If time allows, I will explain some connection with Steve Awodey’s open problem (HoTT workshop 2019) on defining a notion of cubical quasi-category. Some part of this is j.w.w. Fabian Ruch.

Benno van den Berg: Homotopy Type Theory with Explicit Conversions (slides)

Much 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).

Fredrik Nordvall Forsberg: Ordinal Notation Systems for Ordinals below ε₀ in HoTT (slides, preprint)

j.w.w. Nicolai Kraus and Chuangjie Xu I will present multiple ordinal notation systems representing ordinals below ε₀ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. By proving the different systems equivalent, we can transport constructions such as arithmetic operations and properties such as transfinite induction between them using the univalence principle.

Practical information

Venue

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

Accommodation

Full-board accommodation at HdBL Herrsching:

• 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.