Carnegie Mellon University

Spring 2021 program

February 5, Jon Sterling — Normalization for Cubical Type Theory

(J.w.w. Carlo Angiuli) We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. The main difficulty in comparison to conventional type theory is located in a new feature of cubical type theories, the absence of a stable notion of neutral term: for instance, the path application (p @ i) ceases to be neutral within its “locus of instability” ∂(i) and must compute to an endpoint. We introduce a new, geometrically-inspired generalization of the notion of neutral term, stabilizing neutrals by gluing them together with partial computability data along their loci of instability — when the locus of instability is nowhere, a stabilized neutral is a conventional neutral, and when the locus of instability is everywhere, a stabilized neutral is just computability data. Our normalization result is based on a reduction-free Artin gluing argument, and yields an injective function from equivalence classes of terms in context to a tractable language of beta/eta-normal forms. As corollaries we obtain both decidability of judgmental equality, as well as injectivity of type constructors in contexts formed by assuming variables x : A and dimensions i : 𝕀.
Article

February 19, Eric Finster — Types are Internal ∞-Groupoids

I will explain an approach to defining infinitely coherent algebraic structures in type theory by exploiting a universe of structures with explicitly prescribed computation rules. Among the structures which can be defined using these techniques are A_oo-monoids and groups, oo-categories, planar oo-operads (i.e. oo-multicategories) and more. As a special case, one obtains an internal definition of oo-groupoid, and I will describe how to use this setup to describe the type of oo-groupoids explicitly by showing that it is in fact equivalent to the universe U of types. In other words: every type admits the structure of an oo-groupoid internally, and that structure is unique.
Slides of the talk
Article

February 26, No Seminar

March 5, Karol Szumilo — Infinity groupoids in lextensive categories

I will discuss a construction of a new model structure on simplicial objects in a countably extensive category (i.e., a category with well behaved finite limits and countable coproducts). This builds on previous work on a constructive model structure on simplicial sets, originally motivated by modelling Homotopy Type Theory, but now applicable in a much wider context. This is joint work with Nicola Gambino, Simon Henry and Christian Sattler.
Slides of the talk
Article

March 12, Dan Christensen — Non-accessible reflective subuniverses in HoTT

I will review the theory of reflective subuniverses ("localizations") as described in [RSS] and [CORS]. These include modalities such as n-truncation, as well as non-modalities such as localization at a prime. Every small family of maps determines a reflective subuniverse, and the ones determined in this way are called "accessible". I will describe the construction in [CORS] of a new reflective subuniverse L' associated to any reflective subuniverse L, noting that care was taken to avoid the assumption that L is accessible. But are there any interesting non-accessible reflective subuniverses? The second part of the talk will outline a new proof that for a not-necessarily small family of n-connected maps there is still an associated reflective subuniverse, generalizing classical work of Casacuberta, Scevenels and Smith. In order to prove this, I'll prove some results that extend Rijke's join construction [R] to prove that certain types are small.

[CORS] J.D. Christensen, M.P. Opie, E. Rijke, and L. Scoccola. Localization in homotopy type theory. Higher Structures 4(1) (2020), 1-32.
[R] E. Rijke. The join construction.
[RSS] E. Rijke, M. Shulman, and B. Spitters. Modalities in homotopy type theory. Log. Methods Comput. Sci. 16(1) (2020), Paper No. 2, 79 pp.
Slides of the talk

March 19, David Jaz Myers — Modal Fracture for Higher Groups

In his nLab page "Differential Cohesion and Idelic Structure", Urs Schreiber shows how a family of fracture theorems for spectra --- including the traditional fracture theorem of Sullivan and the differential cohomology hexagon of Bunke, Nikolaus, Völkl --- can be expressed through the interplay of an adjoint modality/comodality pair. In this talk, we will construct an unstable version of this modal fracture hexagon in "strongly oo-connected homotopy type theory", which is Mike Shulman's cohesive homotopy type theory without the sharp modality. The modal fracture hexagon relates the universal oo-cover of a higher group with the group's infinitesimal remainder, the quotient of the group by its discrete reflection. Through the course of the talk, we'll meet these two characters and learn of their drama. This tension culminates in the modal fracture hexagon, and our calculation of the homotopy type of the infinitesimal remainder.
Slides of the talk

April 2, Nima Rasekh — Every Elementary Higher Topos has a Natural Number Object

One key aspect of elementary topos theory is the existence of a natural number object. While it does not exist in every elementary topos (such as finite sets) we often need it to study more advanced aspects of topos theory (such as free monoids). In this talk we want to see how in the higher categorical setting, the existence of a natural number object can in fact be deduced from a very small list of axioms that any reasonable definition of elementary higher topos should satisfy, hence proving that every elementary higher topos has a natural number object. We will observe how the main challenge of the proof is not to construct the relevant object, but rather how to prove it has the desired universal property (the Peano axioms) in a higher categorical setting and how we will import ideas from homotopy type theory to overcome this challenge.
Slides of the talk
Article

April 9, Greg Langmead — Several Angles on the Theory of Connections

Homotopy Type Theory provides a means to reinvent existing mathematics. By selecting, or discovering, the right definitions of classical constructions, smart people have imported many structures into HoTT already, thereby simultaneously formalizing the material (often in a computer as well) and vastly generalizing it. So how might we import gauge theory and Chern-Weil theory? These are topics that become available after one has constructed principal bundles. These provide a source of topological invariants, both of bundles and of the base-space manifold as well. They offer obstructions to orientation, nonvanishing vector fields, and other constructions. Consider the Gauss-Bonnet theorem: by integrating the scalar curvature of a connection over a surface, you obtain the Euler characteristic. Moreover gauge theory is the gateway to the standard model of physics, where gauge fields (connections) are the forces and the matter fields are given by sections of associated vector bundles. To unlock all of this we need the theory of connections and curvature on a principal bundle. In this talk I will give an overview of connections _from the classical perspective_. We may speculate together about a HoTT version, but I will not be offering one. The prerequisites are smooth manifolds and tangent bundles (a vague familiarity will suffice). I'll be going breadth-first so I can hasten to show a few different definitions, calling out material that I'm glossing over so that we can circle back in breakout sessions on future occasions.

May 14, Mathieu Anel — An example of elementary ∞-topos

A homotopy type is called bounded coherent if it is truncated and if all its homotopy invariants are finite sets. We shall prove that the ∞-category BCoh(S) of bounded coherent spaces has many of the expected features of elementary ∞-topoi: it is a lex category, with extensive finite sums, and with universal and effective quotients of Segal groupoid objects, it is locally cartesian closed, it has a subobject classifier, enough univalent families and all k-truncation modalities (and all these structures can be computed in the category of all spaces). However, it does not have pushouts and none of the univalent families seems to be closed under ∑ and ∏, which prevent BCoh(S) to be an instance of Shulman's definition of elementary ∞-topos. But, bounded coherent spaces do define a non-trivial universe in the Grothendieck ∞-topos of small spaces.
Slides of the talk

May 21, Fernando Larrain Langlois — A Higher Inductive Presentation of the Integers

Final public examination for the degree:
MASTER OF SCIENCE IN LOGIC, COMPUTATION AND METHODOLOGY:
Advisor: Steve Awodey
Committee: Jonas Frey
1pm, in the Zoom room of the seminar

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