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:

Summer 2022

See our HoTTEST Summer School 2022.

Fall 2022

The schedule for Fall 2022 will be posted here in August 2022.

Past talks

Spring 2022

 Date Speaker Talk information Mar 31 Assia Mahboubi Inria, Nantes Continuity in dependent type theory(joint work with Pierre-Marie Pédrot and Martin Baillon) A result due to M. Escardó establishes the continuity of all functionals definable in Gödel's system T. In this talk, we discuss how to generalize the result to a richer, dependent type theory. Via the construction of a syntactic model, akin to the effectful forcing of Escardó's proof, we obtain an external proof of continuity for any functional |- f : (nat -> nat) -> nat definable in this type theory. Media: slides, no video. Mar 17 Chaitanya Leena Subramaniam University of San Diego Dependently typed algebraic theories and their homotopy algebras Dependently typed algebraic theories are a generalisation of ordinary multisorted algebraic theories (finite-product theories). When it comes to models valued in Set, they are just as expressive as essentially algebraic theories (finite-limit theories). They also combine well with homotopy theory, and have a canonical notion of model up-to-homotopy in spaces, or "homotopy algebra", via a left Bousfield localisation of a global model structure on simplicial presheaves. In this talk, I will consider dependently typed algebraic theories to be a strict subclass of contextual categories. With respect to models valued in Set, this strict subclass is nevertheless just as expressive as essentially algebraic theories. Moreover, contextual categories in this subclass have a nice description of their homotopy algebras, generalising a definition of homotopy algebras of ordinary algebraic theories due to Badzioch and Bergner.Homotopy algebras of ordinary algebraic theories enjoy a rigidification theorem stating that every homotopy algebra is weakly equivalent to a strict simplicial algebra. I will report on recent joint work with S. Henry showing that the same is true for homotopy algebras of dependently typed algebraic theories. This result uses a weak factorisation system introduced by Henry on the category of Set-models of a contextual category, as well as Henry's notion of weak model category.  Media: video, slides. Mar 3 Fredrik Nordvall Forsberg University of Strathclyde Different Notions of Ordinals in Homotopy Type TheoryOrdinals are a powerful tool when justifying induction and recursion, proving that processes terminate, or in mathematics generally. In classical set theory, there are many equivalent ways to introduce them, but in a constructive setting, the different notions split apart, with different advantages and disadvantages for each. I will consider three different notions of ordinals in homotopy theory theory: a "syntactic" notation system based on Cantor normal forms, a quotient inductive-inductive type of Brouwer trees, and wellfounded extensional orders from the HoTT book. Although defined very differently, all three notions have properties expected of ordinals: their order relations are extensional and wellfounded (and thus support transfinite induction), and the usual arithmetic operations can be defined in each case. Furthermore, the notions are connected in the sense that there are structure preserving non-surjective embeddings of Cantor normal forms into Brouwer trees, and of Brouwer trees into wellfounded extensional orders.This is joint work with Nicolai Kraus and Chuangjie Xu. Media: video, slides. Feb 17 Marcelo Fiore University of Cambridge Mathematical and Computational Metatheory of Second-Order Algebraic Theories I will present a further step in my ongoing research programme on Algebraic Type Theory, the overall aim of which is to develop a mathematical theory understanding type theories algebraically while supporting practical foundations. The talk will centre on Second-Order Algebraic Theories, which are equational presentations in languages with (first-order) algebraic type structure and (second-order) term structure with variable-binding operators and parametrised metavariables. Examples include: first-order logic, simply-typed computational calculi, and the calculus of partial differentiation.Specifically, I will present a new categorical model for Second-Order Algebraic Theories: it is based on indexed families and founded upon the initial-algebra approach. A main motivation for and crucial aspect of the mathematical theory is that it is directly programmable in languages supporting inductive families; and, indeed, was developed in unison with building a formally-verified computer implementation for second-order semantics, computation, and deduction. As such, the work resulted in a framework within the Agda proof assistant for the automatic generation of generic second-order abstract syntax and provably correct metaoperations for manipulating it; to wit, algebraic models together with compositional interpretations, capture-avoiding and metavariable substitution operations, and equational and/or rewriting reasoning. This is joint work with Dmitrij Szamozvancev; a paper, source code, documentation, and case studies are available at the project page . Media: video, slides. Feb 3 Jonas Frey Carnegie Mellon University Characterizing clan-algebraic categories Clans provide a categorical notion of dependent algebraic theory that can be seen as syntax-free abstraction of Cartmell’s generalized algebraic theories and as such is closely related to concepts like contextual categories and categories with families. Viewed as algebraic theories, clans are equally expressive as finite-limit theories but contain more information: the same finite-limit theory can have representations by different clans, and in particular different clans can have the same category of Set-models. The additional information encoded in a clan T gives rise to a weak factorization system (E,F) on the locally finitely presentable category Mod(T) (first considered by Henry), from which the clan can be reconstructed up to Morita equivalence. In earlier work I conjectured a characterization of “clan-algebraic categories” -- i.e. lfp categories equipped with a wfs arising as models of a clan -- in terms of an exactness condition that generalizes an analogous characterization of categories of models of ordinary algebraic theories. In this talk I give a proof of this conjecture, and illustrate the exactness condition by means of examples. Media: video, slides. Jan 13 & 20 HoTTEST Event for Junior Researchers 2022

Fall 2021

 Date Speaker Talk information Dec 2 Taichi Uemura Stockholm University ∞-type theories and internal language conjectures HoTT is expected to give internal languages for elementary ∞-toposes. As the first step towards this goal, Kapulkin and Lumsdaine made a precise formulation of the conjecture that dependent type theory with intensional identity types gives internal languages for finitely complete ∞-categories. This simple version of the internal language conjecture is still difficult due to the coherence problem. In ∞-categories, most equations hold up to homotopies, but type theories have a stricter notion of equality, judgmental equality.In this talk, we introduce an ∞-dimensional generalization of type theories which we call ∞-type theories to prove Kapulkin and Lumsdaine's conjecture. An ∞-type theory is like a type theory, but judgmental equality behaves like homotopies rather than strict equality, so there is no coherence problem between ∞-type theories and ∞-categories. The internal language conjecture is then reduced to a coherence problem between the type theory and a suitable ∞-type theory. We solve the new coherence problem by developing a splitting technique for models of the ∞-type theory.An advantage of our approach is that one can easily formulate internal language conjectures for richer type theories, for example type theories with function types, inductive types, and universes. Any internal language conjecture is then reduced to a coherence problem between a type theory and an ∞-type theory. Unfortunately, we have not yet found a general solution to the coherence problem (the splitting technique we present only works for intensional identity types). If time permits, we will discuss possible approaches to the general coherence problem.Joint work with Hoang Kim Nguyen.  Media: video, slides. Nov 18 Raffael Stenzel Masaryk University Higher sites and their higher categorical logic [In the following, read higher'' as (∞,1)-''.] It is a popular idiosyncrasy of higher toposes that, when defined in terms of Giraud-style axioms, a general representation result in terms of higher sheaf categories on a site appears to fail. Essentially, this discrepancy arises because sites'' here are implicitly understood to be higher categories equipped with proof-irrelevant (topo)logical data, while higher toposes are constructions within an intrinsically proof-relevant ambient world. In the first part of the talk, we use this intuition of ambient proof-relevance to further develop the characterization of higher toposes over a given higher base topos in terms of their associated left exact modalities (Appendix of [1], and [2]). We give a definition of higher sites respective a small higher base category C which expresses PreSh(C)-global localization'' in terms of C-indexed nullification'' with respect to an associated sheaf of ideals. In this context I will also mention how one can derive an associated notion of higher Lawvere-Tierney topology as well (which is work in progress). In the second part of the talk, we take a look at examples of such higher sites which are derived from classical examples considered in ordinary categorical logic. We will do so by simply ignoring the artificial propositional truncations implicit to these examples in the ordinary setting, and hence move away from the classical sheaf condition towards more general colimit-preserving properties. Such, so I hope, may be useful in the future for the study of the higher categorical semantics of intensional type theories. [1] Rijke, Shulman, Spitters - Modalities in Homotopy Type Theory [2] Anel, Biedermann, Finster, Joyal - Higher Sheaves Media: video, slides. Nov 4 Kristina Sojakova Inria Paris Syllepsis in Homotopy Type Theory It is well-known that in homotopy type theory (HoTT) one can prove the Eckmann-Hilton theorem: given two 2-loops based at the reflexivity path at an arbitrary point a : A, we have pq = qp. If we go one dimension higher, i.e., if p and q are 3-loops, we show that a property classically known as syllepsis also holds in HoTT: namely, the Eckmann-Hilton proof for q and p is the inverse of the Eckmann-Hilton proof for p and q. Media: video, slides, paper, code. Oct 21 Hugo Moeneclaey IRIF Paris Parametricity and cubes We report on our investigations linking parametricity and cubical structures. Our slogan is that cubical models of type theory are cofreely parametric.Using various notions of parametricity and of models of type theory, we will present the following as cofreely parametric:- Categories with Families (CwF) of semi-cubical types, with Pi-types and a universe.- Categories of cubical object, for any kind of cubes.- CwF of setoids (here seen as 1-dimensional Kan objects), with a univalent universe of propositions.- Clans of Reedy fibrant objects (work in progress).- Tribes of Kan cubical objects (work in progress).We will introduce a notion called interpretation, used to build these cofree objects. Media: video, slides. Oct 7 Matthieu Sozeau Inria Nantes The MetaCoq Project Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implementations. However, proof assistant implementations themselves are seldom formally verified, although they take a major share of the trusted code base in any such certification effort. In this area, proof assistants based on Higher-Order Logic enjoy stronger guarantees than the ones based on Dependent Type Theory, as self-certified implementations have been available for some years. One cause of this difference is the inherent complexity of dependent type theories together with their extensions with (co)-inductive types, universe polymorphism and complex sort or dimension systems. Another is the gap between theory on paper and practical implementations in efficient programming languages. In particular, an efficient implementation of definitional equality checking can be far away from its ideal specification.The MetaCoq project aims to tackle these difficulties in the case of the Coq proof assistant. It provides the first fully-certified realistic implementation of a type checker for the calculus underlying the Coq proof assistant. I will present how we refined the sometimes blurry, if not incorrect, specification and implementation of the system to produce:- A specification of Coq's syntax and type theory, the Polymorphic Cumulative Calculus of (Co)-Inductive Constructions (PCUIC)- A monad for the manipulation of raw syntax and interaction with the Coq system- A verification of PCUIC's metatheory, whose main results are the confluence of reduction, type preservation and principality of typing- A realistic, correct and complete type-checker for PCUICFinally, I will focus on work in progress to relate the current specification of PCUIC to a presentation of type theory with typed equality. http://metacoq.github.io Media: video, slides. Sept 23 Rafaël Bocquet Eötvös Loránd University Coherence of definitional equality in type theory Hofmann has proven that the extension of intensional type theory (with Uniqueness of Identity Proofs) by the equality reflection rule is conservative. For HoTT or other type theories without UIP, we can consider extensions that replace some typal equalities by definitional equalities, such as the extension of HoTT by a strictly associative and unital addition on natural numbers. In this talk I will show that conservativity holds whenever the base type theory satisfies "external univalence" and the definitional equalities added by the extension are coherent, that is when "every formal composition of these equalities is trivial." The formal statements of these conditions involve some type-theoretic infinity-categories, i.e. infinity-categories that are presented by models of type theory.  Media: video, slides.

Spring 2021

 Date Speaker Talk information April 22 Ulrik Buchholtz TU Darmstadt (Co)cartesian families in simplicial type theory Using Riehl–Shulman's simplicial type theory for synthetic higher category theory, I'll describe how to define and work with (co)cartesian families. These represent functors from a higher category to the category of categories. As an application, I'll derive a (dependent) Yoneda lemma for such families. This is joint work with Jonathan Weinberger. Media: video, slides. April 8 Egbert Rijke University of Ljubljana A higher encode decode method The Postnikov tower of a pointed type X induces a fiber sequence $K(G,n+1) -> \|X\|_{n+1} -> \|X\|_n$ for every n, where G is the (n+1)-st homotopy group of X. This fiber sequence suggests a general approach to computations of higher homotopy groups of types, by encoding a family of n-connected (n+1)-truncated types over the type $\|X\|_n$. While I do not yet have any finished computations of homotopy groups of types via this approach, it does suggest a fruitful line of research with interesting intermediate results. Media: video, slides. March 25 Håkon Robbestad Gylterud Universitetet i Bergen Defining and relating theoriesSince the advent of homotopy type theory, many different formal theories for HoTT (such variations of Martin-Löf’s theory, cubical type theory, ⋯) have joined the already plentiful ranks of formal theories. In this talk, we will try to outline a general, algebraic and combinatorial notion of formal theory – geared towards dependent type theories – based on work by Cartmell, Makkai and others.The notion of theory we present is being implemented in a software framework aimed at working with different theories and translations between them, called Myott. Thus, part of the presentation will focus on the Haskell implementation of the theoretical notions. Media: video, slides. March 11 Andrea Vezzosi IT University of Copehagen Cubical Agda and its Extensions Cubical Agda is a dependently typed language with Univalence and Higher Inductive Types based on Cubical Type Theory. In this talk we will see how its features interact with pattern matching, copatterns, and interactive development. We will then introduce the universe of non-fibrant types, where the  interval of cubical type theory lives, and which will let us talk  about strict equality from within the type theory. Finally we will see the extension with a modality for guarded recursion, providing a type-based approach to productivity of corecursive definitions and an abstract way to construct step-indexed models of programming languages.  Media: video, "slides". 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. Media: video, slides. 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.