Higher-order categories in Lean 4
My mathematics degree final project, a formalization of higher-order categories in Lean 4.
This is my final project for the mathematics degree at the Universitat de València, supervised by Enric Cosme Llópez. Higher-order categories are a generalization of ordinary category theory in which morphisms can exist at multiple levels. They play a central role in modern mathematics, particularly in algebraic topology and homotopy theory.
The mathematical content of this project is based on the work by Juan Climent Vidal, Enric Cosme Llópez and Raúl Ruiz Mora in chapter 5 of From higher-order rewriting systems to higher-order categorial algebras and higher-order Curry-Howard isomorphisms. In our project, we reorganized this content so that it can be formalized in Lean 4.
The source code of the formalization is available on GitHub1, where we also host the project page. This page gathers the three things the repository builds: the blueprint, a document that states every definition in ordinary prose and links it to the actual Lean declaration, the same blueprint as a PDF, and the API documentation generated from the docstrings in the code. Finally, the thesis can be found on Zenodo.2
The two presentations of higher-order categories
In our work, two presentations of higher-order categories are studied: the single-sorted and the many-sorted ones.
In the single-sorted presentation, morphisms of every dimension live in a single set . What tells them apart is a family of source and target operations, one pair per dimension, so that a -cell is a morphism that its -th source leaves fixed. Composition at each dimension is partial, and it is defined exactly when the source of one morphism meets the target of the other.
In the many-sorted presentation the dimensions are kept apart from the start. Each dimension has its own set , and the operations run between levels. For every pair of dimensions there are source and target maps that send a -morphism down to a -morphism, an identity map that lifts a -morphism up to dimension , and a partial composition of -morphisms over their common -boundary.
Both presentations are first defined over a finite range of dimensions, which gives the -categories, and then extended by letting the dimensions run over all the naturals, which gives the -categories.
The work also proves that the two presentations are equivalent, and the idea is short to state in either direction. A single-sorted category already carries the grading inside it, since its -cells sit in as a chain of nested subsets, so taking those sets of cells as the carrier of each dimension recovers a many-sorted category. In the other direction, a many-sorted category is collapsed by keeping only its top layer, which already holds a copy of every lower dimension through the identity maps, and defining the operations on it. The two constructions, graduation and unification, turn out to be mutually inverse up to natural isomorphism, so the two presentations are equivalent as categories, first in the finite case and then in the infinite one.
This equivalence is the one part of the work that stays outside the formalization, for reasons discussed further on.
The formalization in Lean 4
The core of our work is the formalization of the structures described above, together with the constructions around them. That is, the functors between them, the categories that single-sorted and many-sorted categories assemble into, and the discretization and underlying transformations. Discretization raises a category to a higher dimension by adding trivial structure above it, and the underlying transformation forgets every dimension past a given one.
Each presentation is defined over a general type of indices and specialized afterwards, so one construction covers the finite and the infinite case at once. A single-sorted category is a class carrying, at each dimension, a source, a target, and a composition that is only defined when the two sides match up:
class CategoryStruct (Index : Type) (C : Type u) where
/-- Source operation at dimension `k`. -/
sc : Index → C → C
/-- Target operation at dimension `k`. -/
tg : Index → C → C
/-- Partial composition operation at dimension `k`. -/
pcomp : Index → C → C →. C
/-- Composition is defined exactly when the sides match up. -/
pcomp_dom : ∀ {k : Index} {f g : C},
(pcomp k g f).Dom ↔ sc k g = tg k f := by hcat_dischFixing the indices to Fin n gives the -categories, and fixing them to ℕ gives the -ones, which need
one further axiom to keep every morphism at a finite dimension:
/-- A single-sorted $n$-category is a `Category` indexed by `Fin n`. -/
abbrev NCategory (n : ℕ) (C : Type u) := Category (Fin n) C
/-- A single-sorted $\omega$-category is a `Category` indexed by `ℕ`, with an
axiom making every morphism a $k$-cell for some finite `k`. -/
class OmegaCategory (C : Type u) extends Category ℕ C where
/-- Every morphism is a $k$-cell for some `k : ℕ`. -/
is_cell : ∀ f : C, ∃ k : ℕ, cell k fThe long lists of axioms are split into a single-dimension core with the cross-dimensional laws layered on top, which keeps the definitions legible and the proofs local. The first block ends in the project’s own discharge tactic, offered as the default value of the axiom. Every axiom is marked as a simplification lemma as it is declared, so each one feeds a shared rule set and most of the routine obligations of later constructions close without a script.
The formalization obstacle
The equivalence is the one piece deliberately left outside the formalization. The thesis states the result and gives the idea of the proof rather than the argument in full. What kept it out of Lean is that in the many-sorted presentation each dimension is a separate type, so an equality between a morphism at one dimension and a morphism at another is no longer an equality in the ordinary sense. Passing between the presentations identifies the set at each dimension with a subtype of the topmost one, and to Lean those are simply different types. On paper the substitution of equals for equals is free. In Lean it becomes an explicit transport along an equality of types, chained across every dimension, which adds no mathematics and a considerable amount of work.
The gap between what prose takes for granted and what a proof assistant requires in full is the main lesson of the project. Much of formalizing is design work. The encoding chosen for a family of types decides whether the later proofs close on their own or turn into bookkeeping, and by the time that becomes clear the encoding is already everywhere.
Status and future work
The thesis is finished, defended and published on Zenodo. The formalization covers both presentations in the finite and the infinite case, their functors, the categories they assemble into, and the discretization and underlying transformations together with their functoriality.
The project continues as my final project for the master’s degree in Mathematical Research, again supervised by Enric Cosme Llópez, and two questions lead that work. The first is the equivalence, which waits on the encoding discussed above. The second is a conjecture the thesis leaves on record, that discretization is left adjoint to the underlying transformation, which would fit both adjunctions into a single algebraic square.