Carnegie Mellon University

All seminars are currently online only:

Meeting ID: 622 894 049
Fridays 1-3pm

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 : 𝕀.

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

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

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

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:
Advisor: Steve Awodey
Committee: Jonas Frey
1pm, in the Zoom room of the seminar

Earlier seminars are listed here.