1 Introduction
1.1 Formalization and this document
A formalization project is an effort to translate mathematical definitions, theorems, and proofs into a formal language that can be checked by a computer program known as a proof assistant. The proof assistant verifies that each logical step is valid, ensuring that the resulting proofs are correct beyond any doubt. In this project, we use Lean 4, a theorem prover and programming language originally developed at Microsoft Research. Lean has a growing mathematical library called Mathlib, which provides a large collection of formalized mathematics that we build upon throughout this work.
This document is a blueprint for the formalization. A blueprint serves as a bridge between traditional mathematical writing and computer-verified proofs: it presents the mathematical content in a human-readable form while linking each definition and theorem to its corresponding formal counterpart in the Lean source code. It also tracks the formalization progress, making it easy to see which parts have been completed and which remain to be done. Refer to the official Lean Blueprint GitHub repository for more information on the blueprint tool.
1.2 Project overview
This project is based on the work by Enric Cosme Llópez and Raúl Ruiz Mora in [ 1 ] . In their work, they define the notion of higher-order categories in two different presentations:
- Single-sorted presentation
All morphisms — objects, 1-morphisms, 2-morphisms, and so on live in a single set. Source, target, and composition operations at each dimension give the set its multidimensional categorical structure.
- Many-sorted presentation
Morphisms of each dimension live in a separate set. For each pair of dimensions \((j, k)\) with \(j {\lt} k\), there are source, target, identity, and composition operations relating the two levels.
For each presentation, the corresponding notion of functor is also defined. With these categories as objects and functors as morphisms, one can construct the categories of single-sorted and many-sorted \(n\)-categories, as well as their \(\omega \)-categorical counterparts.
Two functorial transformations are then introduced for each presentation:
- Discretization
Transforms \(n\)-categories into \(m\)-categories for \(n {\lt} m\) (where \(m\) may be \(\omega \)) by adding trivial higher-dimensional structure.
- Underlying
Transforms \(n\)-categories into \(m\)-categories for \(n {\gt} m\) (where \(n\) may be \(\omega \)) by forgetting the higher dimensions.
Each family of transformations is internally compatible: the discretization functors commute with one another, and the underlying functors commute with one another. Moreover, the underlying transformations form a projective system whose limit is the category of \(\omega \)-categories.
Finally, the two presentations are shown to be equivalent through a pair of functors between single-sorted and many-sorted \(n\)-categories:
- Graduation
Transforms a single-sorted \(n\)-category into a many-sorted one by distributing the morphisms into separate sets according to their dimension.
- Unification
Transforms a many-sorted \(n\)-category into a single-sorted one by collecting all morphisms into a single set.
The composition \(\operatorname{Uf}^{(n)} \circ \operatorname{Gd}^{(n)}\) is the identity functor, while \(\operatorname{Gd}^{(n)} \circ \operatorname{Uf}^{(n)}\) is naturally isomorphic to the identity. This establishes the equivalence of the two presentations for finite-dimensional \(n\)-categories.
It is then shown that, since the underlying transformations form a projective system with the category of \(\omega \)-categories as its limit, this equivalence extends to \(\omega \)-categories as well.
1.3 Project status
This document corresponds to version 0.1.0 of the formalization. At this stage, the project covers:
The single-sorted and many-sorted presentations of higher-order categories, including the categories of \(n\)-categories and \(\omega \)-categories together with their functors.
The discretization and underlying transformations for both presentations, including their functoriality.
The following parts of the project overview remain to be formalized, and are therefore not present in this document:
The internal compatibility of the discretization and underlying families, that is, the fact that each family defines a functor on the relevant index category.
The projective limit description of \(\omega \)-categories in terms of the underlying system.
The graduation and unification transformations between the two presentations, together with the equivalence they establish.
The extension of this equivalence to \(\omega \)-categories.
1.4 Notation and terminology
Throughout this text, the terms category and functor, when used outside the single-sorted or many-sorted framework defined in this work, refer to the standard notions of category theory. In the accompanying Lean 4 formalization, these correspond to the definitions provided by Mathlib.
Following the convention of [ 1 ] , we use the word set throughout this text in the classical mathematical sense. In the accompanying Lean 4 formalization, sets correspond to Lean types, and not necessarily to the Lean implementation of sets. In particular, all notions involving sets in this document, such as families of sets, maps between sets, and so on, are compatible with their counterparts for types in Lean.
We adopt the following standard categorical notation:
\(\mathsf{Cat}\) denotes the category whose objects are classical categories and whose morphisms are classical functors between them.
For a category \(\mathsf{C}\), we write \(\mathsf{C}^{\mathrm{op}}\) for its opposite category.
When a preordered set \((S, \leq )\) appears in a categorical context, it is understood as the category whose objects are the elements of \(S\) and where there is a unique morphism from \(a\) to \(b\) if and only if \(a \leq b\).
The core definitions in this work are parametrized by a general index set, which is then specialized to obtain finite-dimensional and infinite-dimensional categories. We introduce the following notation for this purpose.
If not otherwise specified, we use \(\mathcal{I}\) to denote a set of indices equipped with a preorder relation \({\lt}\). This general setting is used to define the core structures. In practice, the main definitions specialize \(\mathcal{I}\) to either a finite set \(n = \left\{ 0, 1, \ldots , n - 1 \right\} \) or the set \(\mathbb {N}\) of natural numbers.
We write \(\overline{\mathbb {N}}= \mathbb {N}\cup \left\{ \omega \right\} \) for the extended natural numbers, where the top element of the inherited order is the symbol \(\omega \), that is, \(n {\lt} \omega \) for every \(n \in \mathbb {N}\).