Could $\infty$-category theory be taught to undergraduates?

TL;DR

This paper surveys efforts to make $ abla$-category theory more accessible to undergraduates by exploring formal proof methods and univalent foundations, aiming to bridge the gap between ordinary and higher categories.

Contribution

It introduces two programs that simplify $ abla$-category theory: formal proof approaches and univalent foundations, making the subject more approachable for learners.

Findings

Formal proof methods can replicate standard categorical theorems.

Univalent foundations offer a new perspective on $ abla$-categories.

These approaches aim to reduce the complexity of $ abla$-category theory.

Abstract

The extension of ordinary category theory to $\infty$-categories at the start of the 21st century was a spectacular achievement pioneered by Joyal and Lurie with contributions from many others. Unfortunately, the technical arguments required to solve the infinite homotopy coherence problems inherent in these results make this theory difficult for non-experts to learn. This essay surveys two programs that seek to narrow the gap between $\infty$-category theory and ordinary 1-category theory. The first leverages similarities between the categories in which 1-categories and $\infty$-categories live as objects to provide "formal" proofs of standard categorical theorems. The second, which is considerably more speculative, explores $\infty$-categories from new "univalent" foundations closely related to homotopy type theory.