# Homotopy Type Theory Electronic Seminar Talks

Homotopy Type Theory Electronic Seminar Talks is a series of research talks by leading experts in Homotopy Type Theory. The seminar is open to all, although familiarity with Homotopy Type Theory will be assumed. To attend a talk, please follow the instructions below.

# How to attend?

We are using Zoom for the talks. Please install the software and make at least one test call before joining a talk. To join follow the link:

# Spring 2021

 Date Speaker Talk information February 25 Carlo Angiuli Carnegie Mellon University Internalizing Representation Independence with Univalence In programming language theory, the principle of representation independence states that programs indexed by structured types are invariant under a wide range of structure-preserving correspondences. The Structure Identity Principle (SIP) states that constructions in HoTT respect structured isomorphisms, but many instances of representation independence involve non-isomorphic types.In this talk, I will motivate representation independence, explain its connection to proof reuse and transfer, and recall the basics of cubical type theory and the SIP. Then, I will describe our recent work on a relational variant of the SIP that uses HIT quotients to improve representation independence scenarios into  structured isomorphisms and thence equalities of structured types. Our results are formalized in Cubical Agda.Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at  https://dl.acm.org/doi/10.1145/3434293. March 11 Andrea Vezzosi IT University of Copehagen TBA TBA March 25 Håkon Robbestad Gylterud Universitetet i Bergen TBA TBA April 8 Egbert Rijke University of Ljubljana TBA TBA April 22 Ulrik Buchholtz TU Darmstadt TBA TBA

# Past talks

## Spring 2021

 Date Speaker Talk information February 11 Norihiro Yamada University of Minnesota Game semantics of homotopy type theory In this talk, I sketch my recent work on game semantics of homotopy type theory (HoTT). My aim is to extend the BHK-interpretation of Martin-Löf type theory to HoTT so that one can better understand HoTT as a foundation of constructive mathematics. In fact, this game semantics can be seen as a mathematical formalisation of the BHK-interpretation of HoTT: It interprets terms in HoTT as constructive "dialogical arguments" on the truths of formulas, i.e., constructive proofs, and in particular terms of Id-types as constructive proofs on the equality between constructive proofs. Further, the game semantics shows that the extension of HoTT by equational univalence, i.e., the judgemental equality between Id-type on a universe and type equivalence, is consistent, and Markov's principle is independent from this extended HoTT. Media: video, slides. January 28 Thierry Coquand Chalmers University Sheaf models and constructive mathematics In the first part of this talk, I will try to motivate why sheaf models are important for constructive mathematics on a specific example: the existence of the (separable) algebraic closure of a field.This is not trivial constructively since for an arbitrary field, it is in general not decidable if a given polynomial is irreducible or not.  One solution, going back to a short note of André Joyal "Les Théorèmes de Chevalley-Tarski et remarques sur l'algèbre constructive", is to use a suitable (effective) sheaf model in which we can build the algebraic closure. I will explain this model and how it can be used to compute with algebraic numbers.One would like to express such a model using the language of type theory, but this is problematic since the roots of a given polynomial cannot be expressed as a function of the coefficients, and we cannot use strong sum to express existence of roots. This motivates the second part of the talk, where I will present joint work with Fabian Ruch and Christian Sattler on how to extend such sheaf models to sheaf models of (univalent) type theory. One can then express and prove results such that the fact that any Gm-torsor is trivial and start to ask if one can force the line (algebraic closure) to be contractible. Media: video, slides.

## Fall 2020

 Date Speaker Talk information Dec 3 Jamie Vicary University of Cambridge A type theory for strictly unital infinity-categories   Finster and Mimram recently introduced the simple type theory Catt [1], in which terms correspond to cells of a free weak infinity-category on a finite signature. (Alternatively, these terms can be thought of as inhabitants of a directed path type.) We give a decision procedure for determining when two terms are the same "up to units", which we add to the type theory as a definitional equality [2]. This yields a new, strong definition of strictly unital infinity-category, and gives a new type theory Catt_u in which homotopically complex path type inhabitants can be directly constructed, with a vast reduction in complexity compared to the basetype theory. We give some illustrated examples, and speculate about future applications of these ideas to make path types in homotopy type theory easier to handle.[1] Eric Finster and Samuel Mimram (2017), "A Type Theoretical Definition of Weak \omega-Categories",http://arxiv.org/abs/1706.02866.[2] Eric Finster, David Reutter and Jamie Vicary (2020), "A Type Theory for Strictly Unital \infty-Categories",http://arxiv.org/abs/2007.08307. Media: video, slides. Nov 19 Pierre Cagne Universitetet i Bergen On the symmetries of the spheres in univalent foundations In this talk, I will present a joint work with Marc Bezem and Nicolai Kraus that explores the type of symmetries of the n-sphere (n>0), i.e. the type Sn = Sn, in HoTT-UF. I will start by proving that S1=S1 is equivalent to S1+S1. From there, one can try to generalize the result in higher dimensions. I will treat the case n=2 in details and prove that S2=S2 has exactly two connected components, equivalent to one another, with explicit elements (through univalence) for each of the components. The shape of these components though is much more mysterious, but I will outline why we should not expect S2=S2 to be equivalent to S2+S2. From there, and if time permits, I will generalize further by induction on n, and show that Sn = Sn has exactly two connected components for higher n, and I will end on some insights about the shape of these components. Media: video, slides. Nov 5 Nima Rasekh École Polytechnique Fédérale de Lausanne Filter Products and Elementary Models of Homotopy Type Theory One important question in the study of homotopy type theory is the characterization of its models. A crucial step towards solving this problem was taken by Shulman, who proved that we can interpret homotopy type theory in every Grothendieck (∞,1)-topos. In this talk we want to show that his results can be generalized to certain (∞,1)-categories coming from filter products. We will use this result to construct new models of homotopy type theory that are not Grothendieck (∞,1)-toposes.Media: video, slides. Oct 22 Ambrus Kaposi Eötvös Loránd University Quotient inductive-inductive types and higher friends   Quotient inductive-inductive types (QIITs) are generalisations of inductive types where we allow multiple sorts indexed over each other and we allow equality constructors. QIITs can also be seen as initial algebras for generalised algebraic theories.In this talk I will show a simple direct definition of QIITs, explain their categorical semantics and give a survey of the current results about existence of initial algebras.I will also describe two extensions: higher inductive-inductive types and higher order abstract syntax.Joint work with Thorsten Altenkirch, Rafaël Bocquet, András Kovács, and Xie Zongpu. Media: video, slides. Oct 8 at 8 AM EDT Yuki Maehara Macquarie University A cubical model for weak ω-categories   A (strict) ω-category is usually defined as a globular set equipped with compositions. But one can instead consider cubical sets equipped with compositions, and Al-Agl, Brown and Steiner proved that these two notions give rise to equivalent categories. Steiner also showed that, in the cubical setting, the compositions may be encoded in a somewhat indirect manner using open boxes. In this joint project with Tim Campion and Chris Kapulkin, we modify this encoding and propose the resulting objects as a model for weak ω-categories (a.k.a. (∞,∞)-categories). We also construct the Gray tensor product and compare our model to a simplicial precursor, i.e. complicial sets. The aim of this talk is to illustrate the above paragraph with many pictures. Media: video, slides. Sep 24 Jakob von Raumer University of Nottingham Coherence via Well-Foundedness   When mapping out of a quotient into a 1-type, we find ourselves in the situation of needing to prove that a function is coherent in the following way: All cycles in the relation we quotient by are mapped to refl. Proving statements about all cycles is notoriously difficult because it does not straightforwardly admit induction.In practice, we often take quotients by binary relations which resemble reduction relations, and as such are co-wellfounded and locally confluent. In this talk I will show that under these circumstances, we can find an induction principle which can then be used to tackle this kind of coherence problem in HoTT. The main part of the proof is a purely graph theoretic construction, independent from its use in HoTT. This is joint with Nicolai Kraus. Media: video, slides. Sep 10 Guillaume Brunerie and Peter LeFanu Lumsdaine Stockholm University Initiality for Martin-Löf type theory   “Initiality” is the principle that the term model of some type theory should be an initial object in the category of models of that type theory.  Thomas Streicher gave a careful proof of initiality for the Calculus of Constructions in 1991.  Since then, initiality for more complex type theories (such as Martin-Löf type theory) has often been treated as established, as a straightforward extension of Streicher’s result, but never written up carefully for a larger theory.Around 2010, various researchers (notably Voevodsky) raised the question of whether these extensions really were sufficiently straightforward to consider them established without further proof.  Since then, views on the status of initiality have varied within the field; but the issue has been, at least, a frustrating unresolved point.In this talk, we present a proof of initiality for a full-featured Martin-Löf type theory.  The proof is formalised in Agda, to dispel any question of thoroughness (and also partly formalised in Coq), and is carefully designed for extensibility to other type theories.  The proof is based on Streicher’s, using some improvements of Hofmann and further refinements by the present authors.  The two formalisations present slightly different versions of the statement — using contextual categories in Agda, categories with attributes in Coq — but the core of the proof is parallel. Joint work with Menno de Boer and Anders Mörtberg. Media: slides-PLL, slides-GB, video.

## Summer 2020

The HoTTEST Conference of 2020 will take place June 15-19, 2020, only on the internet.

## Spring 2020

 Date Speaker Talk information Apr 16 Matthew Weaver Princeton University A constructive model of directed univalence in bicubical sets Directed type theory is an analogue of homotopy type theory where types represent ∞-categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete fibrations whose directed morphisms correspond to functions—a higher-categorical analogue of the category of sets and functions. In this talk, I’ll present a constructive model of a directed type theory with directed univalence in bicubical, rather than bisimplicial, sets. We formalize much of this model using Agda as the internal language of a 1-topos, following Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete fibrations, with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we refine the universe of covariant fibrations using the constructive sheaf models by Coquand and Ruch. (Joint work with Dan Licata.) Media: video, slides. Apr 2 Denis-Charles Cisinski Universität Regensburg Univalence of the universal coCartesian fibration The model of higher categories given by Joyal's model structure for quasi-categories has univalent universes of coCartesian fibrations. This subsumes the existence of univalent universes of Kan fibrations proved by Voevodsky. Furthermore, the existence of such universes can be used as an alternative to the yoga of homotopy coherent nerves to prove all the essential features of higher category theory, giving a (directed) type theoretic approach to the foundations of higher categories. Media: video, slides. Mar 19 Jon Sterling Carnegie Mellon University Objective Metatheory of Dependent Type Theories What type theorists and other researchers in type theory have in common is that they study theorems that hold of the initial model of type theory; but type theorists especially emphasize the theorems whose statements are sufficiently non-type-theoretic that they need not be preserved by homomorphisms of models. These theorems, sometimes called "metatheorems" or "admissibilities", are the means by which we conceive and justify computerized implementations of type theory, including canonicity, normalization, and decidability of type checking and judgmental equality.The main tool for proving such theorems is Tait's method of computability, which has in the past several years been subject to a rapid campaign of rectification using the categorical language of Artin gluing. I will give an overview of this brave new "objective computability", emphasizing my recent joint work with Angiuli and Gratzer on a general gluing theorem for models of MLTT along flat functors into Grothendieck topoi, with an application to cubical type theory. Media: video, slides. Feb 20 Karol Szumiło University of Leeds The Constructive Kan-Quillen Model Structure The classical Kan-Quillen model structure on the category of simplicial sets is a fundamental object in homotopy theory. Many proofs of its existence have been found, but (until recently) all of them relied on principles of classical logic: the law of excluded middle and the axiom of choice. For the purposes of interpretation of Homotopy Type Theory, such arguments were insufficient.A fully constructive proof is possible, but it requires a careful adjustment of the definitions of cofibrations and weak homotopy equivalences of simplicial sets. In the talk, I will outline one such constructive argument, explaining how various standard techniques of simplicial homotopy theory need to be adapted to constructive logic.This is joint work with Nicola Gambino and Christian Sattler, inspired by Simon Henry who was the first to obtain the result. Media: video, slides. Feb 6 Niels van der Weide Radboud University Constructing 1-Truncated Finitary Higher Inductive Types as Groupoid Quotients In homotopy type theory, one can define spaces, such as the spheres and torus, with higher inductive types (HITs). These types generalize inductive types by allowing constructors for (possibly higher) paths beside constructors for points.One scheme for HITs is defined by Dybjer and Moenclaey. It allows defining HITs by providing arities for constructors for the points, paths, and paths between paths. The arities are allowed to be recursive, but they have to be finitary.In this talk, we show how to interpet the HITs defined by Dybjer and Moenclaey as 1-types using the grorupoid quotient. Concretely, this means we construct finitary 1-truncated HITs as groupoid quotients within type theory. Media: video, slides. Jan 23 Simon Henry University of Ottawa The language of a model category I will explain how to any model category, one can associate a first order language which allows to formulate properties of its fibrant objects that are automatically invariant under homotopies and weak equivalences. For example, the special case of the folk model structure on Cat reproduce the well known result that a first order statement about categories not involving equality of objects is invariant under isomorphisms and equivalences of categories. The construction I will present generalizes this to any model category, for example to spaces or quasi-categories. Though it does not explicitly use it, this is strongly inspired from Makkai's FOLDS and shed a slightly new light on the connection between dependent type theory and homotopy theory. Media: video, slides.

## Fall 2019

 Date Speaker Talk information May 2 Mathieu Anel Carnegie Mellon University Descent v. UnivalenceThe purpose of the talk will be to explain the connection between the notion of descent, characteristic of infinity-topoi, and the notion of univalence, characteristic of homotopy type theory. Media: video, slides. April 18 Paolo Capriotti Technische Universität Darmstadt Polynomial monads as opetopic types In a previous HoTTEST talk, Eric Finster presented a coinductive definition of polynomial monads that should make it possible to formulate higher algebra internally in HoTT. In my talk, I will show how one can connect Finster's construction to the formalism of opetopes and opetopic objects, and its connection with the Baez-Dolan construction for polynomial monads. More precisely, I will give a reformulation of Finster's definition of polynomial monad in terms of opetopic types satisfying a kind of Segal condition. It will turn out that, once the basic notion of trees over a polynomial is established, Finster's coherence for magmas can be expressed purely in terms of polynomials and their maps. This should hopefully provide a first step towards comparing Finster's definition with the established ∞-categorical notion of polynomial monad. Media: video, "slides". April 4 Joachim Kock Universitat Autonoma de Barcelona ∞-operads as polynomial monads I'll present a new model for ∞-operads, namely as analytic monads. This is joint work with David Gepner and Rune Haugseng. In the ∞-world (unlike what happens in the classical case), analytic functors are polynomial, and therefore the theory can be developed within the setting of polynomial functors. I'll talk about some of the features of this theory, trying to focus on aspects that might be of interest to type theory, in particular the construction of free monads, and the relevance of polynomial monads for the semantics of higher inductive types. Media: video, "slides". March 21 Dan Licata Wesleyan University A Fibrational Framework for Substructural and Modal Dependent Type Theories (joint work with Mitchell Riley and Michael Shulman) Modal type theory extends type theory with additional unary type constructors, representing functors, monads, and comonads of various sorts.  For example, the modalities discussed in the HoTT book are idempotent monads, while some recent extensions of HoTT make use of idempotent comonads.  Modal types can be used to speak synthetically about topology and geometry, and also have been used in the internal language semantics of cubical type theories. Over the past few years, we have been working on a general framework for modal type theories. In this framework, specific type theories can be specified by a signature---for example, "type theory with an idempotent monad and an idempotent comonad which are themselves adjoint".  Given a signature, instantiating general inference rules provides a syntax for working with the desired modal types.  While the framework does not automatically produce optimized'' inference rules for a particular modal discipline (where structural rules are as admissible as possible), it does provide a syntactic setting for investigating such issues, including a general equational theory governing the placement of structural rules in types and in terms.  While this is still work in progress, we hope to give a categorical semantics to the entire framework at once, saving the work of considering each modal type theory individually. Media: video, slides. March 7 Evan Cavallo Carnegie Mellon University Internal Parametricity and Cubical Type Theory A polymorphic function is intuitively said to be parametric when it behaves uniformly at all types. This concept was made precise by Reynolds, who defined parametric functions to be those with an action on relations and showed that all polymorphic functions definable in the simply-typed lambda-calculus are parametric. Recently, dependent type theories have been developed that internalize this property, which is known as parametricity; this work is closely connected to cubical type theory, both historically and methodologically. I'll discuss the similarities and differences between internally parametric and cubical type theory, the type theory we designed that combines the two, and potential applications to higher-dimensional theorem proving.This is joint work with Robert Harper, and details can be found in our preprint arXiv:1901.00489. Media: video, slides. February 21 Simon Huber University of Gothenburg Homotopy canonicity for cubical type theory Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral.  A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices.  In this talk I will present why if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.  The proof involves proof relevant computability predicates (also known as sconing) and doesn't involve a reduction relation.This is joint work with Thierry Coquand and Christian Sattler. Media: video, slides. February 7 Nima Rasekh MPI Bonn Algebraic Topology in an Elementary Higher Topos An elementary higher topos is a higher category which should sit at the intersection of three concepts: higher category theory, algebraic topology and homotopy type theory. The goal of this talk is to give concrete examples of these connections.In particular we show how every elementary higher topos has a natural number object, how this can be used to define truncations and how the existence of truncations implies the Blakers-Massey theorem. Media: video, slides. January 31 Nicola Gambino University of Leeds From algebraic weak factorisation systems to models of type theory Algebraic weak factorisation systems are a refinement of the classical weak factorisation systems in which diagonal fillers are given by a prescribed algebraic structure. The notion of an algebraic weak factorisation system was introduced by Marco Grandis and Walter Tholen, and subsequently refined by Richard Garner, who then developed the theory in a series of joint papers with John Bourke. In this talk, I will explain general methods for constructing weak factorisation systems that can be used for defining models of dependent type theory satisfying all the required strictness conditions. This is based on joint work with Christian Sattler and subsequent work in the Leeds PhD thesis of Marco Larrea. Media: slides, no video.