Emily Riehl presents a vision for making infinity category theory accessible to undergraduates by replacing traditional set-theoretic foundations with homotopy type theory, drawing a parallel to how Galois theory—once incomprehensible even to leading mathematicians—became standard undergraduate material after the right abstractions (like groups) were developed.
Why this matters: Infinity category theory is central to modern mathematics (e.g., algebraic topology, derived algebraic geometry, topological quantum field theories), but its current formulations are so technically demanding that they remain inaccessible outside specialized graduate training.
The core idea: Just as category theory unified disparate mathematical results (e.g., properties of inverse images, tensor products, free groups) by abstracting their common structure, infinity category theory captures higher-dimensional homotopical information—but only becomes intuitive when built on a foundation that natively supports homotopy types.
Category Theory as a Unifying Language
Category theory provides a “bird’s eye view” of mathematics by focusing on objects and morphisms (arrows) rather than internal structure, enabling unified proofs across different fields.
Example: The fact that left adjoint functors preserve coproducts explains why:
Inverse images preserve unions and intersections,
Tensor products distribute over direct sums,
Free groups respect disjoint unions.
These share one categorical proof, replacing multiple ad hoc arguments.
Key tools include:
Yoneda lemma: To show two objects are isomorphic, it suffices to show a natural bijection between all maps into them.
Adjunctions: A pair of functors (F, U) where maps from F(C) to D correspond naturally to maps from C to U(D); F is the left adjoint, U the right.
Coproducts: Defined by a universal property—maps out of a coproduct A ∐ B correspond to pairs of maps from A and B.
From Ordinary to Infinity Categories
Ordinary categories have objects and 1-dimensional arrows; equality between arrows is binary (equal or not).
2-morphisms between 1-morphisms (e.g., homotopies between paths),
3-morphisms between 2-morphisms (homotopies between homotopies),
And so on, up to infinity.
Composition is not strictly associative or unital—but associative and unital up to coherent higher equivalences.
Fundamental example: The fundamental ∞-groupoid of a topological space:
Objects: points,
1-morphisms: paths,
2-morphisms: homotopies between paths,
Higher morphisms: higher homotopies.
This captures the full homotopy type of the space (Grothendieck’s homotopy hypothesis).
Many poorly behaved ordinary categories (e.g., derived categories) are better understood as homotopy categories of ∞-categories.
The Problem with Set-Theoretic Foundations
Traditional foundations (ZFC set theory + first-order logic) are ill-suited for ∞-categories because:
They treat equality as strict and binary,
They lack native support for homotopy types or higher coherences.
Existing models of ∞-categories (e.g., quasi-categories, complete Segal spaces) are defined using simplicial sets with complex horn-filling conditions—precise but opaque and far from intuitive.
These definitions require significant background in homotopy theory and are not suitable for undergraduates.
Homotopy Type Theory as a Better Foundation
Homotopy type theory (HoTT) reimagines the foundations of mathematics:
Types replace sets; terms replace elements.
Types are interpreted as homotopy types (∞-groupoids); terms as points.
Identity type Id_A(x, y) represents paths from x to y—not just a truth value, but a space of proofs.
Path induction allows reasoning about all paths by considering only reflexivity (x = x).
Univalence axiom: Equivalence between types is equivalent to identity (A ≃ B) ≃ (A = B).
This makes mathematical constructions automatically invariant under equivalence.
Propositions as types: A theorem is a type; a proof is a term of that type.
Logical connectives correspond to type formers:
A × B ↔ “A and B”,
A → B ↔ “A implies B”,
Σ and Π types ↔ existential and universal quantifiers.
Defining ∞-Categories in Simplicial Type Theory
Simplicial type theory extends HoTT with:
Shapes: Syntactic descriptions of simplices and their boundaries (e.g., Δ¹, ∂Δ², inner horns),
Extension types: Given a function defined on a subshape, the extension type consists of all extensions to a larger shape.
In this system, an ∞-category is a type A where:
For any composable pair of arrows f : x → y and g : y → z, the type of composites g ∘ f is contractible (i.e., uniquely specified up to a contractible space of choices).
This replaces the strict existence-and-uniqueness axiom of ordinary categories.
Identity arrows and associativity are theorems, not axioms—they follow from contractibility.
An ∞-category further requires that the canonical map from paths (identity types) to isomorphisms is an equivalence (completeness).
Key advantage: Naturality conditions (which must be manually verified in set theory) are automatic in HoTT due to its constructive, homotopy-invariant nature.
Revisiting Classical Theorems
The theorem “left adjoints preserve coproducts” carries over directly to ∞-categories:
Coproducts are defined via equivalences of mapping spaces (not bijections of hom-sets),
Adjunctions are defined via equivalences of hom-types,
The same chain of equivalences proves the result—without needing to check naturality.
This demonstrates that ∞-category theory, when built on HoTT, is no more complex than ordinary category theory—only the interpretation of “equality” changes.
Formalization and Future Directions
These ideas have been implemented in a proof assistant called rzk, based on simplicial type theory:
Definitions of pre-∞-categories, composition, identities, and associativity are fully formalized,
Proofs are machine-checked, catching subtle errors (e.g., circular reasoning in early drafts).
This approach lowers the barrier to entry:
Undergraduates could learn ∞-category theory as part of a standard curriculum,
Researchers in other fields (e.g., number theory, symplectic geometry) can use ∞-categorical tools without years of prerequisite study.
Ongoing work aims to formalize more of ∞-category theory in this framework, with collaboration facilitated via Zulip chat platforms.
