A Formalization of Higher-Order Categories in Lean 4

3 Single-sorted discretization transformations

Every single-sorted \(n\)-category can be embedded into a higher-dimensional \(m\)-category by declaring all dimensions above \(n\) to be trivial: sources and targets act as the identity, so composition is only defined between equal morphisms, and we set it to return the morphism itself. This construction extends naturally to the \(\omega \)-categorical setting. Moreover, any single-sorted \(n\)-functor automatically preserves this extended structure, giving rise to a functor between the resulting higher-dimensional categories. We call this process the discretization transformation, and we show that it is functorial and that discretization transformations at different dimensions commute with one another.

3.1 Discrete single-sorted categories

Definition 3.1 Discrete single-sorted finite category

Let \(\mathsf{C}\) be a single-sorted \(n\)-category, and let \(m \in \mathbb {N}\) with \(n {\lt} m\). The discrete \(m\)-category of \(\mathsf{C}\) is the single-sorted \(m\)-category \(\mathsf{C}^{{\gt}m}\) defined on the same underlying set \(C\), where 1 :

  • For \(k {\lt} n\), the source, target, and composition at dimension \(k\) are those of \(\mathsf{C}\).

  • For \(n \leq k {\lt} m\), the source and target at dimension \(k\) are the identity, and composition is defined only between equal morphisms, returning the morphism itself.

Proof

Each axiom either involves only dimensions below \(n\), reducing to the corresponding axiom of \(\mathsf{C}\), or involves a dimension \(k \geq n\), where it trivially follows from the fact that all operations are trivial.

Definition 3.2 Discrete single-sorted omega category

Let \(\mathsf{C}\) be a single-sorted \(n\)-category. The discrete \(\omega \)-category of \(\mathsf{C}\) is the single-sorted \(\omega \)-category \(\mathsf{C}^{{\gt}\omega }\) defined by the same case distinction as in Definition 3.1, now with \(k\) ranging over all of \(\mathbb {N}\).

Proof

The single-sorted category axioms follow by the same argument as in Definition 3.1. The \(\omega \)-categorical axiom holds because \(\operatorname{sc}^n (f) = f\) for every \(f \in C\), so every morphism is an \(n\)-cell.

3.2 Discrete single-sorted functors

Definition 3.3 Discrete single-sorted finite functor

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(n\)-categories, and let \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted \(n\)-functor. For any \(m \in \mathbb {N}\) with \(n {\lt} m\), the same underlying map \(F\) defines a single-sorted \(m\)-functor \(F^{{\gt}m} \colon \mathsf{C}^{{\gt}m} \to \mathsf{D}^{{\gt}m}\).

Proof

Each preservation axiom either involves only dimensions below \(n\), where it follows from \(F\) being an \(n\)-functor, or involves a dimension \(k \geq n\), where it trivially follows from the fact that all operations are trivial.

Definition 3.4 Discrete single-sorted omega functor

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(n\)-categories, and let \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted \(n\)-functor. The same underlying map \(F\) defines a single-sorted \(\omega \)-functor \(F^{{\gt}\omega } \colon \mathsf{C}^{{\gt}\omega } \to \mathsf{D}^{{\gt}\omega }\).

Proof

The argument is identical to that of Definition 3.3.

3.3 Single-sorted discretization functors

The discrete constructions of the previous sections are in fact functorial, as the following definition makes precise.

Definition 3.5 Single-sorted discretization functor

Let \(n, m \in \overline{\mathbb {N}}\) with \(n \leq m\). The discretization functor \(\operatorname{\mathcal{D}}^{(n, m)}\) from \(n\mathsf{Cat}\) to \(m\mathsf{Cat}\) is the functor that maps every single-sorted \(n\)-category \(\mathsf{C}\) to its discrete \(m\)-category \(\mathsf{C}^{{\gt}m}\) and every single-sorted \(n\)-functor \(F \colon \mathsf{C} \to \mathsf{D}\) to its discrete \(m\)-functor \(F^{{\gt}m} \colon \mathsf{C}^{{\gt}m} \to \mathsf{D}^{{\gt}m}\). If \(n = m\), then \(\operatorname{\mathcal{D}}^{(n, n)}\) stands for the identity functor on \(n\mathsf{Cat}\).

Proof

Functoriality follows from the fact that the discrete constructions preserve the underlying map: the identity functor on \(\mathsf{C}\) yields the identity functor on \(\mathsf{C}^{{\gt}m}\), and the composition of two \(n\)-functors yields the composition of their discrete \(m\)-functors.

  1. Since no ambiguity arises, we denote the source, target, and composition operations of \(\mathsf{C}^{{\gt}m}\) by the same symbols as those of \(\mathsf{C}\).