Carnegie Mellon University

 SPRING 2022 program

Fridays 1:30-3:30pm in BH 235A


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

The purpose of this three-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.

February 11, Jonas Frey — Characterizing clan-algebraic categories

Clans provide a categorical notion of dependent algebraic theory that can be seen as syntax-free 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 finite-limit theories but contain more information: the same finite-limit theory can have representations by different clans, and in particular different clans can have the same category of Set-models. 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 “clan-algebraic 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.

February 18, Rio Alvaro JacksonAccessibility, Presentability & Adjointness

The goal of this talk is to provide an introduction to three core topics (as above) central to a more modern approach to category theory. In particular, I will discuss how these centrals notions allow for elegant characterizations and generalizations of well-established patterns in, e.g., algebra in the form of finitely generated abelian groups, as well as providing a workable solution to some size issues. Moreover, I will demonstrate a relatively concise proof of the Adjoint Functor Theorem using these same tools.

February 25, Reid Barton — The rank and size of locally presentable categories

This talk will describe the viewpoint on locally presentable categories as the cocomplete categories that admit small presentations as cocomplete categories. We will discuss the two notions of rank and size of a locally presentable category, and describe how they relate to the various characterizations of locally presentable categories.

March 4 — Sina HazratpourA 2-Categorical Proof of Frobenius in HoTT

In the context of models of HoTT, the Frobenius condition says that the pushforward along fibrations preserve fibrations. This is used for the interpretation of dependent product (Π) types. Coquand gave a simple constructive proof of Frobenius in Cubical Type Theory, taking advantage of the fact that fibration structures can be reduced to composition structures. We give a 2-categorical proof of the Frobenius condition guided by the category-theoretic proofs by Gambino & Sattler and by Awodey. This is based on joint work with Emily Riehl.

March 11 — No seminar (weekend in Claymont)

March 18 — Michele ContenteOn the relationship between MF and HoTT

The goal of this talk is to provide an introduction to the Minimalist Foundation, a two-level type theory introduced by Maietti and Sambin, and to investigate its relationship with HoTT. In particular, I will discuss an interpretation of both levels of MF in HoTT and some problems related to this interpretation. If time permits, I will introduce an extension of MF with rules for inductively generated formal topologies and describe how these rules may be interpreted in HoTT. This is based on joint work (in progress) with Milly Maietti.

March 25 — Steve AwodeyKripkeJoyal semantics for type theory

We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. This is jww/ Nicola Gambino and Sina Hazrathpour, available as arXiv:2110.14576.

April 1 — Maru SarazolaIntroduction to K-theory

This talk will be a brief introduction to algebraic K-theory from a category theorist's point of view; that is, from someone who enjoys to study structures and universal properties much more than computations or concrete applications. We will go over some of the history of algebraic K-theory, starting in the 50's, and moving on to a more modern perspective. After describing several possible inputs for algebraic K-theory, we will define the K-theory of a ring, and show how this can be generalized to define the K-theory of a Lawvere theory.

April 8 — No seminar (ASL meeting)

April 15 — Kian Cho — Introduction to model categories

April 22 — Owen MilnerQuillen equivalence between SSet and Top

April 28 — Mike Shulman — Towards a Third-Generation HOTT (Part 1 of 3)

11:30am-1:00pm EST (UTC-04:00)
Zoom link:
Meeting ID: 622 894 049
Passcode: the Brunerie number

In Book HoTT, identity is defined uniformly by the principle of "indiscernibility of identicals". This automatically gives rise to higher structure; but many desired equalities are not definitional, and univalence must be asserted by a non-computational axiom. Cubical type theories also define identity uniformly, but using paths instead. This makes more equalities definitional, and enables a form of univalence that computes; but requires inserting all the higher structure by hand with Kan operations.

I will present work in progress towards a third kind of homotopy type theory, which we call Higher Observational Type Theory (HOTT). In this system, identity is not defined uniformly across all types, but recursively for each type former: identifications of pairs are pairs of identifications, identifications of functions are pointwise identifications, and so on. Univalence is then just the instance of this principle for the universe. The resulting theory has many useful definitional equalities like cubical type theories, but also gives rise to higher structure automatically like Book HoTT. Also like Book HoTT, it can be interpreted in a class of model categories that suffice to present all Grothendieck-Lurie (∞,1)-toposes; and we have high hopes that, like cubical type theories, some version of it will satisfy canonicity and normalization.

This is joint work with Thorsten Altenkirch and Ambrus Kaposi.

 April 29 — Reid Barton — Finite presentability of homotopy groups of spheres

Serre proved that the homotopy groups of spheres are finitely presented as one application of what we now call the Serre spectral sequence. I will outline a proof of the same theorem using "low-tech" methods. Based on joint work with Tim Campion.

May 5 — Mike Shulman — Towards a Third-Generation HOTT (Part 2 of 3) 

11:30am-1:00pm EST (UTC-04:00)
Zoom link:
Meeting ID: 622 894 049
Passcode: the Brunerie number

May 6 — Wentao Yang — Some relations between μ-abstract elementary classes and accessible categories

We will investigate the relationship between μ-abstract elementary classes, which are generalizations of AECs by requiring only μ-directed unions to exist, and accessible categories, which are categories generated by certain “small” objects under μ-directed colimits.

May 10 — Fernando Larrain Langlois — Normalization of Lambda-calculus

May 11 — Egbert RijkeUnivalent main classes of latin squares

A common theme in combinatorics is to count the number of objects of some kind, up to a naturally defined equivalence relation. A common theme in univalent mathematics is that when you define the type of objects of some kind, then the identity type is a naturally defined equivalence relation. There is clearly a match between these two subjects. I'll illustrate my approach to univalent combinatorics to a definition of the groupoid of main classes of latin squares, in which two latin squares are considered to be equivalent of one can reached from the other by some permutation of the set {r,c,s} denoting the rows, columns, and symbols, and permutations of the rows, columns, and symbols themselves. We will also introduce the notion of pi-finiteness, which can be used to show efficiently that a type has finitely many connected components and to show that all its homotopy groups up to a given level are finite. This notion has been used to construct the OEIS sequence A000001 of the number of isomorphism classes of groups of order n, and the sequence A003090 of main classes of latin squares, among other sequences. Our definitions of these sequences make heavy use of the univalence axiom, and so far any computations using the cubical Agda proof assistant have been unsuccessful.

May 12 — Mike Shulman — Towards a Third-Generation HOTT (Part 3 of 3)

11:30am-1:00pm EST (UTC-04:00)
Zoom link:
Meeting ID: 622 894 049
Passcode: the Brunerie number
Slides, Video

July 12— Chaitanya Leena SubramaniamContexts as computads, linear dependent types, and dependent symmetric multicategories

Certain multisorted algebraic theories (a.k.a. cartesian multicategories) can be described by coloured Set-operads (a.k.a. symmetric multicategories). These are exactly those algebraic theories that are "linear" or "regular" --- namely, they admit presentations by equational theories where for each axiom/equation Γ⊢t=u, every variable of the context Γ appears exactly once in each of the terms t and u. When C is a direct category, finitary monads on [C^op, Set] correspond to certain contextual categories, and these provide a good candidate for the class of "dependent cartesian multicategories". In this talk I will describe work in progress towards characterising the subclass that arise from "dependent symmetric multicategories" or "linear dependently typed algebraic theories". This approach is a generalisation of a technique due to Weber, following Joyal and Girard, that characterises linear multisorted algebraic theories as those whose syntactic categories have "(free,generic)" factorisations. Our work arises from the following observation: while the objects of a contextual category are not necessarily free algebras, they are generalised computads --- and the left maps of the factorisations in question are the computad morphisms. These are better-known as the context morphisms that are variable renamings, and context morphisms that are right orthogonal to them are the elusive "linear dependently typed context morphisms". (joint work in progress with Simon Henry)

August 12— Steve AwodeyAlgebraic type theory (exceptional time 3pm)

A type theoretic universe U* —> U bears an algebraic structure resulting from the type-forming operations of unit type, identity type, dependent sum, and dependent product, which may be generalized to form the concept of a "Martin-Löf algebra". A free ML-algebra is then a model of type theory with special properties. The theory of such ML-algebras can be seen as a proof-relevant version of the theory of Zermelo-Fraenkel algebras from the algebraic set theory of Joyal-Moerdijk. (Work in progress)


Earlier seminars are listed here.