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.
Essential information
 Time: alternate Thursdays at 11:30 AM Eastern (60minute talk + 30minute discussion).
 Mailing list: HoTT Electronic Seminar Talks (for updates) .
 Google Calendar: link.
 Youtube channel: HoTTEST.
 Organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.
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:
Fall 2022
Date & Time 
Speaker  Talk information 
December 1 11:30 Eastern 
Hugo Moeneclaey 
Parametric models for type theory as modules Cubical structures arise naturally when working with parametricity. In our previous HoTTEST talk, we explained this phenomena by arguing that cubical models are cofreely parametric, using a handful of examples. In this talk we present a new framework further strengthening this point of view. We use a symmetric monoidal closed category V of models of type theory (e.g. using categories, lex categories or clans as models). Then we give the following definitions:
Using these simple descriptions, we give the following as examples of cofreely parametric models:

December 1 12 Eastern 
Jacob Neumann 
Allegories and 2Level Directed Type Theory In this talk, I will try to sketch an interesting connection between a few active research areas: the theory of typevalued relations, or 'correspondences'. In the same way that categories provide an abstraction of the algebra of functions and composition, allegories provide an abstraction of binary relations and various operations on them. Combining the concepts of allegory theory with directed type theory, we have an alternate way of defining notions like equivalence and embedding. This promises to be a helpful language for articulating the definitional univalence principle of Higher Observational Type Theory, and in particular provides a clean framework for exploring a directed analogue. We'll explore the theory of correspondences that arises in both an extensional directed type theory, as well as in an intensional directed 2level type theory. 
December 15 11:30 Eastern 
Astra Kolomatskaia 
Why are semisimplicial types hard? When one is first introduced to the informal definition of a semisimplicial type, it immediately strikes one that there is a pattern to the simplex types. This makes one think that the problem is tractable. In this talk we will formally codify, working within homotopy type theory, this apparent pattern via the notion of a simple inverse category. We will then explain how the fundemental problem of semisimplicial types relates to the seeming impossibility of turning a simple inverse category into a type structure. 
December 15 12 Eastern 
Philipp Joram 
Final Coalgebras of Analytic Functors in Homotopy Type Theory In settheoretic foundations, the final coalgebra of a finitary functor can be constructed in (ω+ω) steps [Worrell (2005)]. For particular finitary functors, constructive proofs of this exist, and for polynomial functors it is known that the same can be done constructively in ω steps [Ahrens, Capriotti (2015)]. Similarly, the intermediate class of analytic functors yields final coalgebras in ω steps when working classically. We are interested whether the same is true when working internally to HoTT. We focus our work on the finite multiset functor, a particular analytic functor. One approach is to directly work with a setlevel definition of the functor. This involves proving that it preserves ωlimits. In general, this requires a form of countable choice, which nonetheless seems to be satisfied for the limits involved in the construction of the final coalgebra. We present an alternative construction following [Kock (2012)]. Here, we define a polynomial functor over a groupoid, and show that its pointwise settrunctation is equivalent to the ordinary finite multiset functor. We construct its final coalgebra as an ωlimit, and show that it has as a fixedpoint a type of finitely branching, nonwellfounded trees. While the truncation of this type of trees is a fixedpoint of the ordinary multiset functor, proving that it is the largest fixedpoint requires another choice principle. In the process, we give multiple formalizations of finite multisets in HoTT, one as type of lists modulo permutations, and another one as the HIT of the free commutative monoid, and connect these to prior work, e.g. [Choudhury, Fiore (2021)]. To overcome sizeissues, we port [Finster et al. (2021)]'s axiomatization of a small type of finite sets and bijections to cubical Agda. [Ahrens, Capriotti (2015)]: https://doi.org/10.4230/LIPIcs.TLCA.2015.17 [Worrell (2005)]: https://doi.org/10.1016/j.tcs.2004.12.009 [Kock (2012)]: https://doi.org/10.1016/j.entcs.2013.01.001 [Choudhury, Fiore (2021)]: https://arxiv.org/abs/2110.05412 [Finster et al. (2021)]: https://arxiv.org/abs/2112.14050 
Past talks
Date  Speaker  Talk information 
November 17  Jarl G. Taxerås Flaten 
Central Hspaces and banded types We give a simple description of the type of Hspace structures on a pointed type A. If A is an Hspace, we obtain an untruncated version of a formula of ArkowitzCurjel and Copeland for counting Hspace structures on a space. This formula underlies the classical computations of the number of Hspace structures on various spaces. As an example, we easily deduce that the type of Hspace structures on the 3sphere is equivalent to the sixfold loop space of the 3sphere. Our formula for the type of Hspace structures on A leads us to define and study what we call "central" types, which are generalisations of EilenbergMac Lane types. Central types admit a unique Hspace structure which can be explicitly delooped by a tensor product of "types banded by A." Given an abelian group A, we iterate this process to give an independent construction of K(A,n) along with a description of its Hspace structure that is useful for certain cohomology computations. These results are part of joint, ongoing work with Ulrik Buchholtz, Dan Christensen, David Jaz Myers, and Egbert Rijke. Most of the results have been formalized using the CoqHoTT library. 
November 17  Tom de Jong 
Acyclic types and epimorphisms in HoTT It is well known that the epimorphisms in the category of sets are exactly the surjections. But what are the epimorphisms of types? Thinking of types as spaces, and following literature in algebraic topology, we characterise epimorphisms of types in HoTT as socalled acyclic maps. An acyclic map is a map whose fibres are acyclic types, and a type is acyclic if its suspension is contractible. We also consider a weaker notion: a type is kacyclic (for k ≥ 2) if its suspension is kconnected. We show, for example, that the classifying type of a group G is 2acyclic if and only if the group G is perfect, i.e. its abelianisation is trivial. Finally, we comment on the relations between acyclic and connected maps and sketch directions for future research. This is joint work with Ulrik Buchholtz and Egbert Rijke. 
November 3  Colin Zwanziger 
HofmannStreicher Universes via Coalgebra HofmannStreicher universes (Hofmann and Streicher 1999) are a standard tool for modeling universes in presheaf models of dependent type theory. They have been used in the semantics of HoTT, e.g. in the cubical set model of Cohen et al. (2015). Hofmann and Streicher (op. cit.) noted that their approach to universes does not extend from presheaf models to arbitrary sheaf models. In this talk, we nevertheless extend the approach of Hofmann and Streicher to sheaf models *with enough points*. Consequently, we can handle many sheaf models without resorting to alternatives such as the stack semantics of Coquand et al. (2020). In particular, any model of sheaves on a topological space has enough points. Our approach will be to recover any sheaf model with enough points as a 'topos model of coalgebras' for an appropriate notion of comonad. This construction 'lifts' the universe in the topos model carrying the comonad to the sheaf model in question, yielding a HofmannStreicher universe. Our 'topos model of coalgebras' is a refinement of the wellknown topos of coalgebras (Kock and Wraith 1971). 
November 3 
Evan Cavallo 
Cubes with one connection and relative elegance Given a cube category with cartesian structure (faces, degeneracies, diagonals, and permutations), we know that its category of presheaves supports (constructively!) both an interpretation of homotopy type theory and a compatible Quillen model structure. Here we consider the cube category with cartesian structure and one connection. I will present a proof that the model structure obtained for this cube category is Quillen equivalent to the KanQuillen model structure on simplicial sets. The obstacle to overcome is that this cube category is not a Reedy category: its morphisms do not factor into wellbehaved "degeneracy" and "face" maps. We observe that it does, however, embed in a Reedy category in a nice way. We adapt the theory of socalled elegant Reedy categories to this relativized case, then use these results to prove the equivalence with simplicial sets. This is joint work with Christian Sattler. 
October 20 
Axel Ljungström 
Calculating a Brunerie Number In his PhD thesis, Brunerie defined the notorious 'Brunerie number'  an integer n such that the fourth homotopy group of the 3sphere is isomorphic to Z/n. He then managed to, with a lot of machinery, prove that n = 2. In an ideal world, this part of the proof is unnecessary: the fact that n = 2 should follow immediately by normalising n in a constructive proof assistant like Cubical Agda. In the real world, however, it's not that easy: Cubical Agda is too slow. So we have two obvious choices: we either give up, or we formalise all of Brunerie's original proof (me and my supervisor, Anders Mörtberg, have accepted both options at different points in time). Recently, however, I found a third option: even though normalisation doesn't work, there is still a very direct way of showing that n = 2. In fact, with my definition of n, we can show that n = 2. In this talk, I will give a sketch of this argument. If time permits, I will mention why this argument also shows that the fourth homotopy group of the 3sphere is a subgroup of Z/2. 
October 20 
Max Zeuner 
A univalent formalization of affine schemes Schemes are the corner stone of modern algebraic geometry and have been formalized in various proof assistants. However, the most prominent existing formalizations all follow the inherently nonconstructive approach of Hartshorne's classic "Algebraic Geometry" textbook. Working in Cubical Agda, we want to give a constructive formalization of affine schemes in a univalent setting. We follow an approach due to Coquand, Lombardi and Schuster that uses a pointfree description of the Zariski spectrum but otherwise proceeds by defining the structure sheaf on basic opens first and then lifting it to the whole spectrum. In this talk we will focus on the construction of the structure sheaf on basic opens as it is at this point that working in a univalent setting raises perhaps surprising issues while at the same time offering insightful solutions. 
October 6  Amélia Liao 
Univalent Category Theory Category theory is the study of structure across mathematics. Being a mathematical subject itself, category theory should also encompass the study of its own structural aspects. A promising approach (Gray 1974; Di Liberti & Loregian 2019) is formal category theory: studying the properties of the bicategory of categories which make it possible to study category theory from a structural perspective. A different idea is to approach categories as groupoids with extra structure, something which finds itself naturally at home in HoTT, where "groupoids" are particular types. This approach lends itself particularly well to formalization in a proof assistant. In the context of Cubical Agda, we recap the basic theory of univalent categories (Ahrens, Kapulkin & Shulman 2013) and the move towards higher univalent category theory (Capriotti & Kraus 2017; Ahrens et all 2019), particularly the application of cubical syntax to fibred categories (following Sterling & Angiuli 2021; Ahrens & Lumsdaine 2017). 
October 6  Chris Grossack 
Where are the open sets? Comparing HoTT with Classical Topology It's often said that Homotopy Type Theory is a synthetic description of homotopy theory, but how do we know that the theorems we prove in HoTT are true for mathematicians working classically? In this expository talk we will outline the relationship between HoTT and classical homotopy theory by first using the simplicial set semantics and then transporting along a certain equivalence between (the homotopy categories of) simplicial sets and topological spaces. We will assume no background besides some basic knowledge of HoTT and classical topology. 
Summer 2022
See our HoTTEST Summer School 2022.
Spring 2022
Date 
Speaker 
Talk information 
Mar 31 
Assia Mahboubi Inria, Nantes 
Continuity in dependent type theory 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 (finiteproduct theories). When it comes to models valued in Set, they are just as expressive as essentially algebraic theories (finitelimit theories). They also combine well with homotopy theory, and have a canonical notion of model uptohomotopy 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. 
Mar 3 
Fredrik Nordvall Forsberg University of Strathclyde 
Different Notions of Ordinals in Homotopy Type Theory 
Feb 17 
Marcelo Fiore University of Cambridge 
Mathematical and Computational Metatheory of SecondOrder 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 SecondOrder Algebraic Theories, which are equational presentations in languages with (firstorder) algebraic type structure and (secondorder) term structure with variablebinding operators and parametrised metavariables. Examples include: firstorder logic, simplytyped computational calculi, and the calculus of partial differentiation. 
Feb 3 
Jonas Frey Carnegie Mellon University 
Characterizing clanalgebraic categories Clans provide a categorical notion of dependent algebraic theory that can be seen as syntaxfree 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 finitelimit theories but contain more information: the same finitelimit theory can have representations by different clans, and in particular different clans can have the same category of Setmodels. 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 “clanalgebraic 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.

Jan 13 & 20 

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. 
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 Giraudstyle 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 proofirrelevant (topo)logical data, while higher toposes are constructions within an intrinsically proofrelevant ambient world. In the first part of the talk, we use this intuition of ambient proofrelevance 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 ``Cindexed 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 LawvereTierney 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 colimitpreserving 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 
Nov 4 
Kristina Sojakova Inria Paris 
Syllepsis in Homotopy Type Theory It is wellknown that in homotopy type theory (HoTT) one can prove the EckmannHilton theorem: given two 2loops 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 3loops, we show that a property classically known as syllepsis also holds in HoTT: namely, the EckmannHilton proof for q and p is the inverse of the EckmannHilton 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 semicubical types, with Pitypes and a universe.  Categories of cubical object, for any kind of cubes.  CwF of setoids (here seen as 1dimensional 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. 
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 HigherOrder Logic enjoy stronger guarantees than the ones based on Dependent Type Theory, as selfcertified 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. 
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. 
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. 
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 nconnected (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. 
March 25 
Håkon Robbestad Gylterud Universitetet i Bergen 
Defining and relating theories 
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. 
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 structurepreserving correspondences. The Structure Identity Principle (SIP) states that constructions in HoTT respect structured isomorphisms, but many instances of representation independence involve nonisomorphic types. 
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 BHKinterpretation of MartinLö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 BHKinterpretation 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 Idtypes 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 Idtype on a universe and type equivalence, is consistent, and Markov's principle is independent from this extended HoTT. 
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 ChevalleyTarski 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. 
Fall 2020
Date 
Speaker 
Talk information 
Dec 3 
Jamie Vicary University of Cambridge 
A type theory for strictly unital infinitycategories
Finster and Mimram recently introduced the simple type theory Catt [1], in which terms correspond to cells of a free weak infinitycategory 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 infinitycategory, 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 base 
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 nsphere (n>0), i.e. the type S^{n} = S^{n}, in HoTTUF. I will start by proving that S^{1}=S^{1} is equivalent to S^{1}+S^{1}. From there, one can try to generalize the result in higher dimensions. I will treat the case n=2 in details and prove that S^{2}=S^{2} 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 S^{2}=S^{2} to be equivalent to S^{2}+S^{2}. From there, and if time permits, I will generalize further by induction on n, and show that S^{n} = S^{n} has exactly two connected components for higher n, and I will end on some insights about the shape of these components. 
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.

Oct 22 
Ambrus Kaposi Eötvös Loránd University 
Quotient inductiveinductive types and higher friends
Quotient inductiveinductive 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. 
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 AlAgl, 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. 
Sep 24 
Jakob von Raumer University of Nottingham 
Coherence via WellFoundedness
When mapping out of a quotient into a 1type, 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. This is joint with Nicolai Kraus. 
Sep 10 
Guillaume Brunerie and Peter LeFanu Lumsdaine Stockholm University 
Initiality for MartinLö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 MartinLö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. Joint work with Menno de Boer and Anders Mörtberg. Media: slidesPLL, slidesGB, video. 
Summer 2020
The HoTTEST Conference of 2020 will take place June 1519, 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

Apr 2 
DenisCharles Cisinski Universität Regensburg 
Univalence of the universal coCartesian fibration The model of higher categories given by Joyal's model structure for quasicategories 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. 
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 nontypetheoretic 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. 
Feb 20 
Karol Szumiło University of Leeds 
The Constructive KanQuillen Model Structure The classical KanQuillen 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. 
Feb 6 
Niels van der Weide Radboud University 
Constructing 1Truncated 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. 
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 quasicategories.
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.

Fall 2019
Date 
Speaker 
Talk information 
Dec 11, 4 PM Eastern 
Richard Garner Macquarie University 
Polynomial comonads and comodules To any locally cartesian closed category E one can associate a monoidal category Poly(E) of polynomials; it is (following von Glehn) the fibre over 1 of the free fibration with distributive sums and products on E, or equivalently (following Gambino and Kock) the category of polynomial endofunctors of E. A result of Ahman and Uustalu shows that comonoids in Poly(E) (i.e., polynomial comonads) are the same as internal categories in E. It is then natural to ask: what is the bicategory of comonoids and bicomodules in Poly(E)? The goal of this talk is to explain the (slightly surprising) answer. 
Nov 20 
Benno van den Berg University of Amsterdam 
Uniform Kan fibrations in simplicial sets An important question in homotopy type theory is whether the existence of a model of univalent type theory in simplicial sets (and a model structure) can be proven constructively (say, in CZF with some inaccessibles). One approach would be to take the usual definition of a (trivial) Kan fibration as one's starting point and see how far one gets: this is the approach followed by Henry, Gambino, Szumilo and Sattler in recent work. It turns out that you can get quite far, but some issues remain (especially around the interpretation of Pitypes and coherence). Together with Eric Faber, I am pursuing a different approach in which we add uniformity conditions to the notion of a Kan fibration (as in the cubical sets model). The idea is that classically these conditions can always be satisfied, but not necessarily constructively. This has also been tried by Gambino and Sattler in earlier work, but in our view there are quite a few conditions missing in their definition of a uniform Kan fibration. In this talk, I will try to explain what our definition is, why we believe our definition is better (the idea is that we can prove, constructively, that it is "local"), and how far we are right now. 
Nov 6 
Andrew Swan Carnegie Mellon University 
Choice, Collection and Covering in Cubical Sets In homotopical models of type theory such as cubical sets, propositional truncation has a rich structure. Instead of "identifying points," as in more traditional interpretations of extensional type theory in regular locally cartesian closed categories, one inductively adds new paths, while keeping existing points separate. This extra structure can be particularly clearly exposed by exploiting the fact that cubical sets are valid in a constructive metatheory, and assuming Brouwer's continuity principle, which is an anticlassical axiom stating that all functions from Baire space to the naturals are continuous. In this setting even very weak versions of the axiom of choice, such as WISC and a version of countable choice due to Escardo and Knapp, turn out to be false in the cubical set model. I will also talk about some very weak consequences of countable choice that are false in the model. This includes countable versions of collection and fullness from set theory (providing a solution to exercise 10.12 of the HoTT book). I will also talk about a couple of examples from homotopy theory: the product of countably many copies of the circle is not covered by any hSet and there are examples of hSets that are not covered by any constant cubical set. 
Oct 23 
Anders Mörtberg Stockholm University 
Unifying Cubical Models of Homotopy Type Theory (j.w.w. Evan Cavallo, Andrew Swan) In recent years a wide variety of constructive cubical models of homotopy type theory have been developed. These models all provide constructive meaning to the univalence axiom and higher inductive types, but how are they related? In the talk I will give an answer to this question in the form of a generalization that covers most of the cubical models. The crucial idea of this generalization is to weaken the notion of fibration from the cartesian cubical set model so that it is not necessary to assume that the diagonal on the interval is a cofibration. This notion of fibration also gives rise to a model structure, generalizing earlier work on constructing model structures from cubical models of homotopy type theory. 
Oct 9 
Andrej Bauer University of Ljubljana 
General type theories There are many variants of dependent type theory, but it is difficult to find a complete and exact account of what a type theory is, as a formal system. We shall give a precise definition of what a type theory is in general, as a formal system whose components are various syntactic entities. The syntax of terms and types is described by a signature. Arbitrary inference rules are too unwieldy, so we next identify two properties that an acceptable rule must have. We similarly study what makes a family of rules into an acceptable type theory. To test the quality of our definition we prove fundamental metatheorems about general type theories: JOINT WORK WITH: 
Spring 2019
Date  Speaker  Talk information 
May 2 
Mathieu Anel Carnegie Mellon University 
Descent v. Univalence 
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 BaezDolan 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. 
April 4 
Joachim Kock Universitat Autonoma de Barcelona 
∞operads as polynomial monads

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 signaturefor 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. 
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 simplytyped lambdacalculus 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 higherdimensional theorem proving. 
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 noncanonical 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. 
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. 
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. 
Fall 2018
Date  Speaker  Talk information 
December 6 
Eric Finster Inria  Rennes 
Towards Higher Universal Algebra in Type Theory I will propose a definition of "coherent cartesian polynomial monad" in type theory. Special cases of the proposal yield definitions of ∞operads, ∞categories and ∞groupoids. In addition, I describe a definition of coherent algebra over such a monad, leading to a proposed internal description of objects such as E_{n}types and diagrams of types valued in the universe. 
November 22 
Floris van Doorn University of Pittsburgh

Towards Spectral Sequences for Homology
Spectral sequences form a powerful tool which can be used to compute homotopy, homology and cohomology groups of a wide variety of spaces. We have constructed two important spectral sequences in homotopy type theory, the AtiyahHirzebruch and Serre spectral sequences for cohomology. These spectral sequences have analogues for homology, but they have not been constructed in HoTT yet. However, many parts of our construction could be reused to construct the corresponding spectral sequences for homology.
In this talk I will introduce spectral sequences and review the spectral sequences we have constructed and some of their applications. Furthermore, I will describe what parts are still missing to construct the AtiyahHirzebruch and Serre spectral sequences for homology.
The construction of the spectral sequences for cohomology is joint work with Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Egbert Rijke and Mike Shulman.

November 8 
Guillaume Brunerie Stockholm University 
Computergenerated proofs for the monoidal structure of the smash product The smash product is a very useful operation in algebraic topology and it can be defined in HoTT as a certain higher inductive type. One of its basic properties is the fact that it is a (1coherent) monoidal product on pointed types, but proving this fact turns out to be very technical. I will present some work in progress aiming at proving it via some form of higher dimensional rewriting and metaprogramming. The idea is to write an (untrusted) external program to generate a formal proof, which can then be formally checked by a proof assistant.

October 25 
Nicolai Kraus University of Nottingham 
Some connections between open problems I will give an overview of my plan to construct connections between several unsolved questions. The following are important constructions that we would like to perform internally in type theory: 
October 11 
KuenBang Hou (Favonia) University of Minnesota 
Towards efficient cubical type theory Cubical type theory attracted much attention in the homotopy type theory community because it achieved canonicity in the presence of univalence and higher inductive types. To date, there are many variants of cubical type theory and experimental proof assistants based on them. 
September 27 
Dimitris Tsementzis Rutgers University

FirstOrder Logic with Isomorphism Firstorder logic with isomorphism (“FOLiso”) is a formal system which relates to HoTT and the Univalent Foundations in a similar way that firstorder logic with equality relates to ZFC and settheoretic foundations. In particular, FOLiso gives a precise framework in which to study “firstorder" theories defined on homotopy types (e.g. precategories, univalent categories), just as firstorder logic with equality gives a precise framework in which to study firstorder structures and theories defined on sets. I will first introduce the syntax and proof system of FOLiso as an extension of M. Makkai’s FOLDS. Then I will define a semantics for FOLiso in terms of homotopy types and describe a proof of soundness and completeness for this semantics. I will conclude by sketching applications in various directions. Media: video, slides. 
September 20 
Andy Pitts University of Cambridge 
Axiomatizing Cubical Sets Models of Univalent Foundations 
Spring 2018
Date  Speaker  Talk information 
May 24 
Thierry Coquand University of Gothenburg 
A survey of constructive models of univalence 
May 10 
Thorsten Altenkirch University of Nottingham 
Towards higher models and syntax of type theory

April 26  Martín Hötzel Escardó
University of Birmingham 
Constructive mathematics in univalent type theory I want to share my experience of doing constructive mathematics in univalent type theory, compared to my previous experience in e.g. elementarytopos type theory (as in Lambek and Scott), MartinLöf type theory, Bishop mathematics. 
April 12 
Michael Shulman University of San Diego 
Type 2theories Homotopy type theory is hypothesized to be an internal language for (∞,1)toposes. However, recent developments suggest that more than this, what is needed is an internal language for collections of several (∞,1)toposes together with functors between them, such as adjunctions, monads, comonads, noncartesian monoidal structures, and so on. For instance, a cohesive (∞,1)topos comes with an adjoint triple of two monads and a comonad, while a tangent (∞,1)topos comes with a monad that is also a comonad and also a noncartesian "smash product" monoidal structure. Just as ordinary homotopy type theory is a "doctrine" or "2theory" for (∞,1)toposes, each such situation should come with its own "2theory": a dependent type theory with extra information characterizing the additional structure. But developing even one dependent type theory formally is a lot of work, so we would like a general framework and a general theorem that can then simply be specialized to all such 2theories. I will sketch such a framework, which is under development in joint work with Dan Licata and Mitchell Riley. 
March 29 
Ulrik Buchholtz Technische Universität Darmstadt 
From Higher Groups to Homotopy Surfaces Homotopy type theory can be seen as a synthetic theory of infinity groupoids. From this perspective, the pointed, connected types represent infinity groups. The elements are those of the loop space, and the operations on identity types provide the higher group structure.
In this talk, I'll explain what basic group theory looks like from this viewpoint. One aspect is that of categorifying ordinary group theory by using a univalent universe to present many groups. For example, the cyclic group on n elements is the loop space of the type of nelement sets equipped with a cyclic ordering.
In the second half of the talk, I'll focus on the 2dimensional orthogonal group, and use this to talk about the homotopy types of surfaces.
The talk follows the synthetic approach to homotopy theory as developed in the HoTT book. Beyond that, a basic familiarity with ordinary group theory and the result on the classification of surfaces from topology will be helpful.
Some of the material will be from arXiv:1802.04315 (joint with Floris van Doorn and Egbert Rijke) and arXiv:1802.02191 (joint with Favonia), and some material is brand new.

March 15 
Carlo Angiuli Carnegie Mellon University 
Computational semantics of Cartesian cubical type theory Dependent types are simultaneously a theory of constructive mathematics and a theory of computer programming: a proof of a proposition is at the same time a program that executes according to a specification. Homotopy type theory reveals a third aspect of dependent types, namely their role as an extensible formalism for reasoning synthetically about objects with homotopical structure. Unfortunately, axiomatic formulations of univalence and higher inductive types disrupt the computational character of type theory, which pivots on a property called canonicity. I will discuss Cartesian cubical type theory, a univalent type theory in which the canonicity property holds, based on a judgmental notion of cubes with diagonals, faces, and degeneracies, and uniform Kan operations that compute according to their types. I will consider it primarily through the lens of its computational semantics, defined using a cubical generalization of the technique of logical relations, which licenses reading proofs as programs. This talk is based on joint work with Favonia and Robert Harper, described in arXiv:1712.01800. Some familiarity with the syntax and rules of type theory will be very helpful; I will not assume knowledge about computational semantics or logical relations.

March 1 
Emily Riehl Johns Hopkins University 
The synthetic theory of ∞categories vs the synthetic theory of ∞categories Homotopy type theory provides a “synthetic” framework that is suitable for developing the theory of mathematical objects with natively homotopical content. A famous example is given by (∞,1)categories — aka “∞categories” — which are categories given by a collection of objects, a homotopy type of arrows between each pair, and a weak composition law. In this talk we’ll compare two “synthetic” developments of the theory of ∞categories — the first (joint with Verity) using 2category theory and the second (joint with Shulman) using a simplicial augmentation of homotopy type theory due to Shulman — by considering in parallel their treatment of the theory of adjunctions between ∞categories. Afterwards, I hope to launch a discussion about what considerations might motivate the use of homotopy type theory in place of classical approaches to prove theorems in similar settings. Ideal background: some familiarity with notions of a (ordinary strict 1)category, functor, natural transformation, and the definition of an adjunction involving a unit and a counit (just look these up on wikipedia). Plus standard type theory syntax and the intuitions from the CurryHowardVoevodsky correspondence. I’ll be talking about (∞,1)categories but won’t assume familiarity with them. 
February 15 
Peter LeFanu Lumsdaine Stockholm University 
Inverse diagram models of type theory Diagram models are a flexible tool for studying many logical systems: given a categorical model C and index category I, one hopes that the diagram category C ^{I} will again be a model. For the case of intensional type theory, this becomes a little tricky. Since most logical constructors (e.g. Σtypes, Idtypes) are not provably strictly functorial, it is difficult to lift them from structure on C to structure in C ^{I}, for arbitrary I. However, in case I is an inverse category — roughly, something like the semisimplicial category Δ _{I} — this difficulty can be surmounted by taking the types of C ^{I} to be Reedy types, analogous to Reedy fibrations in homotopy theory. I will discuss the construction of these models (and slightly more general homotopical diagram models) in the setting of categories with attributes, along with the application of these models to the “homotopy theory of type theories”. The work of this talk is joint work with Chris Kapulkin, in arXiv:1610.00037 and a forthcoming companion article; see also Shulman arXiv:1203.3253 for a closely related construction. A basic familiarity with categorical models of type theory will be helpful, i.e. categories with attributes or similar; see here for an introductory overview of these. 