Fall 2020 program
September 11, Steve Awodey — The equivariant model structure on cubical sets
The category of cubical sets has a model structure that can be described axiomatically in a way that is inspired by the model of type theory that it supports. Univalence, for example, plays a key role. This model category is not Quillen equivalent to the standard Kan one on simplicial sets, however. But there is another model structure taking the symmetries of the cubes into account, and that one is equivalent, according to a result by Christian Sattler. In this talk I will explain this more refined "equivariant model structure". Joint work with Thierry Coquand and Emily Riehl.
Slides of the talk
September 18, Thierry Coquand — Descent data operations and constructive sheaf models of type theory
This talk will present a higher generalisation of Lawvere-Tierney modalities that appear naturally in the setting of constructive presheaf models of type theory with univalence axiom and higher inductive types. Using the elementary and essentially algebraic character of these models, they relativise to any presheaf models over a base category. Any Grothendieck topology on this base category gives then rise to a family of modal operations on types, that we can call “descent data operations”. One main result is that these operations are left exact modalities (and each universe of modal types is itself modal). Even in the case of a trivial topology, the associated descent data operation may be non trivial and defines a new internal model where equivalences are pointwise equivalences. (This is closely connected to the recent use of the “cobar” operations by Mike Shulman.) If time allows, we will end with some questions connected to an example where the base site has already been used for an effective definition of the separable closure of a field and for which we should be able to recover, in a constructive setting the cohomological interpretation of the Brauer group of this field.
Notes of the talk
September 25, Jonathan Weinberger — Cocartesian fibrations in Simplicial Type Theory
In 2017, Riehl and Shulman introduced Simplicial Type Theory (STT) which is an extension of Homotopy Type Theory allowing to reason not only about infinity-groupoids, but infinity-categories. A key gadget are judgmental extension types, based on ideas by Lumsdaine and Shulman, allowing for defining directed hom types. The prime model is the infinity-topos of simplicial spaces, hence STT can be seen as a synthetic language for simplicial infinity-groupoids which allows for reasoning about infinity-categories interpreted as Rezk spaces. We discuss aspects of the theory of cocartesian fibrations in this setting. This is joint work with Ulrik Buchholtz.
Slides of the talk
October 2, Simon Henry — Left, right and weak model structures
Left semi-model structure, right semi-model structure and weak model structure are weakening of the notion of Quillen model structures that are still enough to formalize homotopy theory categorically, but are often easier to construct and enjoys better stability properties. I will review these notions, how they relates to each other and to other framework for categorical homotopy theory. This will include several recent or new results about construction of left, right and weak model structure that generalizes known results about Quillen model structure, and tends to be simpler.
Slides of the talk
October 9, Nicolai Kraus — Internal ∞-Categories with Families
It is natural to formalize the notion of a model of type theory (especially the syntax = intended initial model) inside type theory itself. This is often done by writing the definition of a category with families (CwF) as a generalized algebraic theory. What could be the success criterion from a HoTT point of view? The typical first goal is that the initial model is an h-set or even has decidable equality. Our second goal is to make the "standard model" work, i.e. the universe U should be a CwF in a straightforward way (cf. Mike Shulman's 2014 question whether the n-th universe in HoTT models HoTT with n-1 universes). Unfortunately, it is hard to combine these two goals. If we include set-truncatedness explicitly in the definition of a CwF, then the "standard model" is not a CwF. If we don't, then the initial model is not an h-set. The root of the problem is that 1-categories are not well-behaved concepts in an untruncated setting. The natural approach are higher categories, which corresponds to "equipping the syntax with all coherences" instead of truncating. In this talk, I will explain one approach to this based on a type-theoretic formulation of Segal spaces, expressed in HTS/2LTT. I will discuss what works and what is still open. The talk will be based on arXiv:2009.01883.
October 16, Andrew Swan — The Nielsen-Schreier Theorem in Homotopy Type Theory
The Nielsen-Schreier theorem states that subgroups of free groups are themselves free groups. Although the statement of the theorem is simple, it is quite tricky to give a direct proof. However there is a conceptually clear proof using ideas from algebraic topology. This makes the Nielsen-Schreier theorem an ideal candidate for formalisation in homotopy type theory. I will use the characterisation of groups in homotopy type theory as pointed connected 1 truncated types. Under this characterisation it is known that free groups are exactly wedges of circles and that subgroups correspond to pointed connected covering spaces (i.e. families of hSets indexed by the group). With these definitions the ideas of the algebraic topology proof can be applied directly. I will give a constructive proof of the special case of finite index subgroups and a proof of the full theorem using the axiom of choice. The finite index version has been verified electronically using Agda. I will show the axiom of choice is necessary for the full theorem by giving an example of a boolean infinity topos where it is false. A related argument shows that the "untruncated" version of the theorem is provably false in HoTT even for finite index subgroups of finitely generated free groups.
Preprint arXiv:2010.01187 and Agda formalization
October 23, Denis-Charles Cisinski — The ∞-category of ∞-categories
This is a report on a joint work with Hoang Kim Nguyen which establishes a new way to construct the straightening/unstraightening correspondence in the context of quasi-categories.
October 30, Ivan Di Liberti — Formal Model Theory and Higher Topology
Motivated by the abstract study of semantics, we study the interaction between topoi, accessible categories with directed colimits and ionads. This theory amounts to a categorification of famous construction from general topology: the Scott topology on a poset and the adjunction between locales and topological spaces. This technology is then used in order to establish syntax-semantics dualities. Among the significant contributions, we provide a logical understanding of ionads that encompasses Makkai ultracategories.
Slides of the talk
November 6, Joachim Kock — Decomposition spaces, incidence algebras and Möbius inversion
I'll start rather leisurely with a review of incidence algebras and Möbius inversion, starting with the classical Möbius function in number theory, then incidence algebras and Möbius inversion for locally finite posets (Rota) and monoids with the finite decomposition property (Cartier-Foata), and finally their common generalisation to Möbius categories (Leroux). From here I'll move on to survey recent work with Gálvez and Tonks taking these constructions into homotopy theory. On one hand we generalise from categories to infinity-categories in the form of Rezk-complete Segal spaces, taking an objective approach working directly with coefficients in infinity-groupoids instead of numbers. (Under certain finiteness conditions, numerical results can be obtained by taking homotopy cardinality.) On the other hand we show that the Segal condition is not needed for these constructions: it can be replaced by a weaker exactness condition formulated in terms of the active-inert factorisation system in Delta. These new simplicial spaces we call decomposition spaces: while the Segal condition expresses composition, the new condition expresses decomposition. (An equivalent notion, formulated in terms of triangulations of polygons, was discovered independently by Dyckerhoff and Kapranov under the name unital 2-Segal space.) Many convolution algebras in combinatorics arise as the incidence algebra of decomposition spaces which are not categories, for example Schmitt's chromatic Hopf algebra of graphs or the Butcher-Connes-Kreimer Hopf algebra of trees. The Waldhausen S-construction of an abelian (or stable infinity-) category is another example of a decomposition space; the associated incidence algebras are versions of (derived) Hall algebras. I will finish with some recent applications to free probability (joint work with Ebrahimi-Fard, Foissy, and Patras).
November 13, Anders Mörtberg — Programming and proving with the structure identity principle in Cubical Agda
One of the most striking consequences of univalence is the structure identity principle (SIP) which states that equivalent structured types are identifiable. There are multiple ways to formalize this principle in homotopy type theory and I will discuss a variation that we have recently formalized in Cubical Agda. The constructive nature of cubical type theory allows us to reap the full benefits of the SIP, making it possible to transport programs and proofs along paths constructed using the SIP without losing computation. We furthermore generalize the SIP to encompass also relational representation independence results. By using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them the correspondence becomes an equivalence between the quotiented types, thereby allowing us to obtain an equality of implementations by the SIP. We have applied this to a wide variety of examples in the Cubical Agda library, including algebraic structures, unary and binary numbers, matrices, queues, and finite multisets. (This is joint work with Carlo Angiuli, Evan Cavallo and Max Zeuner. Preprint can be found at arXiv:2009.05547.)
Slides of the talk
November 20, Tslil Clingman — More than merely composition: towards the theory of proof-relevant categories and algebras
Homotopy Type Theory has profited immensely from the key insight that precisely how two things are equal is important. This has, in some areas, liberated the mathematician from the necessity of making choices and performing the complex combinatorial computations of manipulating presentations of objects and their equalities. By analogy, in Category Theory many questions of coherence arise when we are forced to choose a `the' composite for some given morphisms. One approach to remedy these issues is by means of addressing composites by their universal property. However, the theme of this talk is that such a stance is not analogous to the key insight of Homotopy Type Theory. Rather, as we will propose, the analogous view would entail that the universal property of a composite ought to be data, and tracking precisely how the universal property is implemented should be important. To that end, in this talk we will introduce the idea of proof-relevant categories and proof-relevant functors with the explicit aim of capturing such data. The former objects are (potentially infinite dimensional) category-like structures in which, for a given arrangement of composable cells, there may be in general many proofs that the arrangement interprets to another cell via composition. The latter objects suitably generalise the anafunctors of Makkai to this setting: on a given input, there may be in general many proofs that the functor obtains a given value. We will strive to motivate these structures by examples, and make connections to the univalent categories of Homotopy Type Theory. These notions all emerge from the general framework of proof-relevant algebras for globular T-categories. Time and interest allowing we will examine how an arbitrary strict omega-category X may be combined with a T-category A so that proof-relevant algebras over the result are proof-relevant algebras for A with proof-relevant morphisms ``in the shape of X''. From this point of view we will consider `compositions' of proof-relevant functors as well as progress towards an appropriate proof-relevant category of proof-relevant categories.
Slides of the talk
December 4, Colin Zwanziger — Sheaf Universes via Coalgebra
There is a well-known construction of a universe for presheaf models of type theory, which does not extend to arbitrary sheaf models (Hofmann and Streicher 1999). This issue is naturally understood in the context of a framework such as natural models of type theory (Awodey 2012). We would like to leverage the fact that any sheaf topos arises as the category of algebras for a Cartesian reflector on a presheaf category. Unfortunately, it is not the case that natural models are closed under the construction of algebras for the corresponding notion of Cartesian reflector (c.f. Coquand et al. 2020). In my dissertation work, I show that natural models are closed under the construction of *co*algebras for Cartesian comonads. This construction generalizes the presheaf case in a direction that includes many sheaf toposes. I will focus in this talk on the example of sheaves on a topological space. We will use a coalgebraic presentation of sheaves. This is similar to the local homeomorphism presentation, but with the advantage that the inverse image of sheaves is strictly coherent (Marmolejo 1998). The natural model and universe structures can be described in relatively familiar terms.
Slides of the talk
December 11, Sina Hazratpour — Kripke-Joyal semantics for dependent type theory
Every topos has an internal higher-order intuitionistic logic. The so-called Kripke–Joyal semantics of a topos gives an interpretation to formulas written in this language used to express ordinary mathematics in that topos. The Kripke–Joyal semantics is in fact a higher order generalization of the well-known Kripke semantic for intuitionistic propositional logic. In this talk I shall report on joint work with Steve Awodey and Nicola Gambino on extending the Kripke–Joyal semantics to dependent type theories, including homotopy type theory.
Slides of the talk
Previous talks in 2020
- April 3: Reid Barton (Pitt), Model Categories for o-Minimal Homotopy Theory
- March 27: Mathieu Anel (CMU) Clans from Lurie’s Geometries
- March 4: Samuele Maschio (Padua) The Minimalist Foundation and Axiomatic Set Theories
- February 28: Milly Maietti (Padua) Compatibility of the Minimalist Foundation with Homotopy Type Theory
- February 21: Jonas Frey (CMU), Duality for Clans
- February 14: Colin Zwanziger (CMU), Generalizing the Topos of Coalgebras to the Natural Model of Coalgebras
- February 7: Reid Barton (Pitt), The Algebra of Combinatorial Premodel Categories
- January 31: Steve Awodey (CMU), A Cubical Universe of Fibrations
- January 17: Jon Sterling (CMU), Gluing Models of Type Theory Along Flat Functors
talks in 2019
- December 6: Jonas Frey (CMU), Categories of Partial Equivalence Relations as Localizations
- November 22: Mathieu Anel (CMU), A Small Object Argument for Unique Factorization Systems
- November 15: Evan Cavallo (CMU), Modelling Identity Types with a Fibred Factorization System
- October 11: Andrew Swan (CMU), Lifting Problems and Algebraic Weak Factorisation Systems over a Grothendieck Fibration
- October 4: Jonathan Weinberger (Darmstadt), Modalities and Fibrations for Synthetic (∞,1)-Categories
- May 3: Greg Langmead (CMU), Categories and Modalities for Smoothness: Part 2
- April 26: Adam Millar (CMU), The Groupoid Model; Zesen Qian (CMU) Induction and Coinduction
- April 19: Anders Mortberg (CMU), UniMath – Univalent Foundations of Mathematics
- March 29: Jonathan Sterling (CMU), Algebraic Type Theory and the Gluing Construction
- March 22: Mathieu Anel (CMU), Small Objects and Their Arguments
- March 11-15: Geometry in Modal Homotopy Type Theory (workshop)
- February 28: Loïc Pujet (Nantes), Synthetic Homotopy Theory in Cubical Type Theory and the Hopf Fibration
- February 22: Iosif Petrakis (LMU Munich), Dependent Sums and Products in Bishop Set Theory
- February 15: David Spivak (MIT), A Higher-Order Temporal Logic for Dynamical Systems
- February 8: Bruno Bentzen (CMU), Informal Cartesian Cubical Type Theory
- February 1: Steve Awodey (CMU), A Quillen Model Structure on the Cartesian Cubical Sets
- January 25: Colin Zwanziger (CMU), Modal Categories with Attributes: Part 2
- January 18: Felix Wellen (CMU), Covering Spaces in Modal HoTT
talks in 2018
- December 14: Colin Zwanziger (CMU), Modal Categories with Attributes: Part 1
- December 7: Siva Somayyajula (CMU), Perspectives on Sessions
- November 30: Koundinya Vajjha (Pittsburgh), Voevodsky’s Simplicial Modal of HoTT
- November 21: Egbert Rijke (UIUC), The Small Object Argument in Terms of the Pushout-Product.
- November 20: David Jaz Myers (Johns Hopkins)
- November 16: Adam Millar (CMU), The Groupoid Model as a Category with Families
- November 9: Greg Langmead (CMU), Categories and Modalities for Smoothness
- November 2: Steve Awodey (CMU), Lax and Strict Models of Dependent Type Theory
- October 25: Marcelo Fiore (Cambridge), 2-Dimensional Lambda Calculus
- October 5, 12, 19: Jonas Frey (CMU), Semantics of Type Theory
- September 21, 28: Mathieu Anel (CMU), Type Theory v. Higher Category Theory
- September 7: Max Doré (LMU Munich) and Colin Zwanziger (CMU), Intension and Extension in Type Theory
- April 27: Dan Christensen (Western Ontario), Vector Fields on Spheres
- April 13: Colin Zwanziger (CMU), Intensional Predicates in Comonadic Intensional Type Theory
- April 6: Marcelo Fiore (Cambridge), An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
- March 8: Andrew Pitts, Pursuing Univalence with Categorical Logic
- February 16: Mathieu Anel (Paris), What’s New in oo-Topoi?
- February 8: Eric Finster (Paris), Lex Modalities in Type Theory
- February 6, 13: André Joyal (Montreal), Theory of Tribes.
- February 2: Felix Wellen (CMU), Algebraic Geometry and Modal Type Theory
- January 26: Joseph Helfer (Stanford), First-Order Homotopical Logic
- January 19: Felix Wellen (CMU), Fiber Bundles in HoTT
- January 15: Ian Orton (Cambridge), An internal presentation of cubical models
talks in 2017
- December 8: Marco Larrea (Leeds), Models of Martin-Löf Type Theory from Algebraic Weak Factorisation Systems
- November 3, 10, 17: Anders Mörtberg (CMU), Introduction to Cubical Type Theory.
- October 20: Simon Boulier (Nantes), Model Structure on the Universe in a Two Level Type Theory
- October 13: Felix Wellen (CMU), Differential Homotopy Type Theor
- September 22: Clive Newstead (CMU), Polynomials, Representability and Dependent Type Theory
- September 1: Pino Rosolini (Genova), Dominance