CMU HoTT Graduate Student Workshop 2021

The 2021 CMU HoTT Graduate Student Workshop is a meeting to exchange ideas related to homotopy type theory, logic, and category theory. The workshop will consist of a series of presentations, with opportunities for discussion. All are welcome to attend. This event is meant to be friendly and informal, and talks on work in progress and unfinished ideas are welcome.

For more information, please contact Jonas Frey.

Speakers

Schedule

Time Speaker Title
11:00-11:45 Jonathan Weinberger A Yoneda Lemma for Synthetic Fibered ∞‑Categories
11:45-12:30 Fernando Larrain Langlois A Higher Inductive Presentation of the Integers
12:30-13:15 Wes Caldwell Sphere Bundles and Characteristic Classes
13:15-13:45 break
13:45-14:30 Colin Zwanziger Lawvere's Law as an Elimination Principle for Identity Types
14:30-15:15 Jacob Neumann Allegories and Bisimulations
15:15-16:00 Chris Grossack Categories, Modalities, and Type Theories: Oh my!

Abstracts

Caldwell — Sphere Bundles and Characteristic Classes. Some of the most powerful techniques in algebraic topology revolve around the construction and manipulation of characteristic classes. In this talk, we will develop the basic theory of characteristic classes in homotopy type theory, focusing specifically on the Thom & Euler classes developed for sphere bundles. As an application of this machinery, we sketch a proof of Serre's finiteness theorem of the homotopy groups of spheres.

Grossack — Categories, Modalities, and Type Theories: Oh my! Category theory and logic have a tight interplay, with structured categories providing semantics for certain logics, and "internal logics" providing a useful language for speaking about structured categories. In this introductory talk we will survey both directions of this correspondence from the point of view of modal logic.

Larrain Langlois — A Higher Inductive Presentation of the Integers. The purpose of this work is to explore the higher inductive nature of the integers in the context of Homotopy Type Theory. We characterize it in terms of familiar category-theoretic notions and formalize the results in the proof assistant Agda. In particular, we formally verify that the integers are equal to the higher inductive type generated by a point and an autoequivalence.

Neumann — Allegories and Bisimulations. Functions and binary relations are two of the most important concepts in modern mathematics. Basic category theory, accordingly, has the category Set of sets and functions and the category Rel of sets and binary relations as standard examples. But, of these two, Set is much more famous and Rel receives relatively little attention. And it's not hard to see why: Set possesses many of the canonical constructions in category theory ((co)limits, exponentials, a subobject classifier, etc.), whereas Rel, for the most part, doesn't. In this talk, I attempt to make the case that Rel has some interesting and worthwhile structure of its own, and put a name to some of its key features. This will take us on a tour through the theory of allegories, which are a kind of categorical structure articulating the essential features of a "category of relations". We'll see some interesting other examples of allegories, and use the allegory structure to define several notable classes of morphisms. I'll conclude by tracing a connection to several different kinds of (classical propositional) modal logic, and indicating interesting questions for further consideration.

Weinberger — A Yoneda Lemma for Synthetic Fibered ∞‑Categories. In 2017, Riehl and Shulman have introduced simplicial homotopy type theory as an extension of HoTT, allowing for reasoning about ∞-categories. We present a notion of fibered ∞-category in this setting. As an application, we argue that this satisfies a Yoneda Lemma whose statement and proof follows Riehl–Verity's (much more general, but not per se homotopy type-theoretical) work on model-independent higher category theory. This generalizes Riehl--Shulman's work from discrete to categorical fibers. This is joint work with Ulrik Buchholtz.

Zwanziger — Lawvere's Law as an Elimination Principle for Identity Types. As noted by Awodey (2016), the principle of path induction closely resembles Lawvere's Law (LL), Lawvere's category-theoretic characterization of equality. However, the iterated type dependency involved in path induction is puzzling from the perspective of LL. I argue that LL corresponds most closely to the principle of path recursion, including a propositional uniqueness principle. While path recursion is a priori weaker than path induction, I show that the two principles are equivalent, adapting an argument of Escardó (2015). Thus, identity types are completely characterized by LL.