# 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.

**When:**Friday, 26 February 2021, 11am - 4pm**Where:**On Zoom. Meeting ID: 919 9162 5799, Passcode: hott2021

## Speakers

- Wes Caldwell (Carnegie Mellon University)
- Chris Grossack (University of California, Riverside)
- Fernando Larrain Langlois (Carnegie Mellon University)
- Jacob Neumann (Carnegie Mellon University)
- Jonathan Weinberger (Technische Universität Darmstadt)
- Colin Zwanziger (Carnegie Mellon University)

## 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.