Emily Riehl Makes Infinity Categories Elementary

In this three-part episode of 'Theories of Everything,' mathematician Emily Riehl presents a visionary framework for making infinity category theory accessible to undergraduate students through the lens of homotopy type theory (HoTT). She begins by demonstrating how category theory unifies diverse mathematical phenomena—such as colimit preservation by left adjoints—through abstraction, using tools like the Yoneda Lemma and natural isomorphisms. Riehl then introduces infinity categories as higher-dimensional structures where equality is replaced by invertible homotopies, exemplified by the fundamental infinity groupoid of a space. She argues that traditional set-theoretic foundations obscure the intuitive essence of these concepts, while HoTT—where types are spaces and proofs are paths—offers a more natural, computationally verifiable foundation. In the second segment, she deepens this vision by exploring dependent types, identity types, and path induction, showing how iterated equalities naturally yield infinity groupoids and how pre-infinity categories can be defined with composition and associativity emerging as theorems rather than axioms. The formalization of these ideas in the RASC proof assistant underscores the practical potential of HoTT for rigorous, machine-checkable mathematics. The final segment features Riehl’s reflections on simplicial type theory and invites listeners to join active Zulip communities around Lean and RASC, while host Curt Jaimungal promotes his new Substack, listener support options, and a partnership with The Economist, which offers exclusive editorial insights through a new podcast series.