The corpus has looked at infinity in 277 of its files. All of it is vertical — countable to uncountable to inaccessible to Mahlo to hyper-Mahlo, each level larger than the last. The infinity of this rung is horizontal, and the series has never used it.
| Chapter 1's infinity | This rung's infinity | |
|---|---|---|
| what it counts | size of a set | dimension of a morphism |
| the ladder | ℵ₀ → 2ℵ₀ → inaccessible → Mahlo → hyper-Mahlo | objects → 1-morphisms → 2-morphisms → 3-morphisms → ⋯ |
| can be small? | no — each level is strictly larger | yes — an ∞-category may have three objects |
| in the corpus | 277 files (geometry), 171 (AXLE) | ≈ 0 by any spelling |
Measured 2026-08-29 across ten spellings including ∞-categor,
quasi-categor, bicategor, Kan complex, nerve,
homotopy coherent and n-morphism. DATA
Chapter 4 supplies an associator and asks it to satisfy the pentagon — a condition on the nose at level 2. If the pentagon itself only holds up to an invertible 3-morphism, the structure is a tricategory, and the same question recurs one level up. The point of an ∞-category is to stop asking: coherence at every level, with no level privileged as the one where equality finally arrives.
Quasi-categories are the standard model and Mathlib has them:
SimplicialSet/ 68 files, quasicategory 6, nerve 7, Kan complex 2, measured on the
build in the geometry repository. This chapter is buildable today in a way rungs 28 and 32 are not.
A decision, argued rather than assumed, about whether the series needs coherence past level 2 at all. "No" is a legitimate and probable answer, and stating it with reasons is worth more than an unused simplicial apparatus.