Carnegie Mellon University

 Fall 2021 program

The live HoTT Seminar is back!
Fridays 1-3pm in BH 235A

September 10, Reid Barton — TBA

September 17, Mathieu Anel — Localizations of categories (part 1)

I will review a number of results around localizations of categories, both in the context of 1‑categories and ∞‑categories. The purpose is to present homotopy theory as a toolbox to compute within ∞‑localizations, as developped in Cisinski's book. (The talk will go over some of the material presented here.)

September 24, Jacob Neumann — Groundwork to Higher Allegory Theory

I will enumerate several interesting possible avenues of research which connect the theory of binary relations to Homotopy Type Theory. Binary relations are indispensable in classical mathematics, and higher-dimensional analogues of binary relations promise to occupy an important (and interesting!) place in univalent mathematics. After rehearsing some of the theory of allegories in the setting of homotopy type theory (and speculating about possible generalizations), I'll discuss how we can adapt certain allegory-theoretic notions to better describe and reason about constructions in type theory. If possible, I hope to also touch on some semantic considerations related to this work, as well as describe some circumstances in functional programming and type theory where binary relations are particularly helpful. The content of this talk is all very much work-in-progress, so suggestions & feedback are very welcome!

October 1, Mathieu Anel — Localizations of categories (part 2)

October 8, Mathieu Anel — Localizations of categories (part 3)

October 15, No seminar (MURI Meeting)

October 22, Kian Cho — Lifting properties and the small object argument

In this talk we will discuss lifting properties of collections of morphisms in a category. Given a class of morphisms, we can define another class of maps that have left lifting property with respect to the given class. We will show such classes are closed under common categorical constructions such as retracts, pushouts, and compositions. We will also define weak orthogonal systems and weak factorization systems and see when a given collection of morphisms can be promoted to a weak factorization system, and as a corollary, when we can obtain a (strict) factorization system.

October 29, No seminar

November 5, Jonas Frey — The fat small object argument

I will discuss ideas around the *fat small object argument*, focussing especially on the "finitary" version that is relevant to the theory of clans.

November 12, Andrew Swan — W Types with reductions in presheaf categories (part 1)

Inductively defined types are ubiquitous in mathematics. It is very common to specify a type or set by listing ways to construct new elements from families of old elements. A simple example is the set of natural numbers, which is inductively generated as the smallest set satisfying the following: There is a natural number 0, and for every natural number n, there is a successor S n. The most natural way to phrase inductive types in category theory is via W-types, which are initial algebras of endofunctors of a certain simple form (called polynomial endofunctors). The small object argument is almost, but not quite an inductively defined type. It is not enough to keep adding new elements: you have to simultaneously do some quotienting for the argument to work. This makes it not an inductive type, but a *higher* inductive type. W types with reductions are a simple kind of higher inductive type that suffice to carry out an internal version of the small object argument, as well as some other constructions, such as localisations of cubical sets. They work very similar to W types, except that in place of algebras for endofunctors we use algebras for *pointed* endofunctors. I'll give an explicit construction of a special case of W types with reductions in presheaf categories. The argument is designed to work in settings where we don't have exact quotients, so we need to only use quotienting in a very limited way. We also avoid using universes or replacement, by using W types in our metatheory instead of regular ordinals. Several explicitly given constructions in cubical sets by Coquand and Huber can be seen as special cases of this one argument.

November 19, Andrew Swan — W Types with reductions in presheaf categories (part 2)

December 3, Carlo Angiuli — Normalization, logical frameworks, and the LCCC of judgments (part 1)

The purpose of this two-lecture series is to provide some general background for the normalization result for cubical type theory recently established by Sterling and myself (
I will begin by defining (reduction-free) normalization, and motivating its importance to the implementation of proof assistants. Next, I will recall Awodey's natural models of type theory and explain how the internal language of a presheaf topos is a "logical framework" in which one can define the theory of MLTT with connectives. Then, I will review Uemura's representable map categories and second-order generalized algebraic theories, before concluding with the locally Cartesian closed category of judgments, a perspective recently advocated by Gratzer and Sterling.

December 10, Carlo Angiuli — Normalization, logical frameworks, and the LCCC of judgments (part 2)


Earlier seminars are listed here.