A Formalization of Higher-Order Categories in Lean 4

4 Single-sorted underlying transformations

Every single-sorted \(n\)-category contains a lower-dimensional \(m\)-category obtained by restricting to the \(m\)-cells: one can show that the source, target, and composition operations preserve the set of \(m\)-cells, so we may consider their birestrictions to it. This construction extends naturally to the \(\omega \)-categorical setting. Moreover, any single-sorted \(n\)-functor maps \(m\)-cells to \(m\)-cells, so it restricts to a functor between the resulting lower-dimensional categories. We call this process the underlying transformation, and we show that it is functorial.

4.1 Underlying single-sorted categories

We begin by showing that, for any dimension \(k {\lt} m\), the source, target, and composition operations at dimension \(k\) of a single-sorted category can be birestricted to the set of \(m\)-cells.

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f \in \mathsf{C}\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), we have that \(\operatorname{sc}^k (f)\) is a \(m\)-cell in \(\mathsf{C}\).

Proof

Applying Axiom 2.3.1, we have that

\[ \operatorname{sc}^m (\operatorname{sc}^k f) = \operatorname{sc}^k (f). \]
Corollary 4.2

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(k \in \mathcal{I}\) such that \(k {\lt} m\), the source operation \(\operatorname{sc}^k\) birestricts to the set of \(m\)-cells \(C_m\).

Proof

Follows directly from Lemma 4.1.

Lemma 4.3

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f \in \mathsf{C}\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), we have that \(\operatorname{tg}^k (f)\) is a \(m\)-cell in \(\mathsf{C}\).

Proof

Applying Axiom 2.3.1, we have that

\[ \operatorname{tg}^m (\operatorname{tg}^k f) = \operatorname{tg}^k (f). \]

That is, \(\operatorname{tg}^k (f)\) is a target-based \(m\)-cell in \(\mathsf{C}\). However, we know that every target-based \(m\)-cell is also a \(m\)-cell.

Corollary 4.4

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(k \in \mathcal{I}\) such that \(k {\lt} m\), the target operation \(\operatorname{tg}^k\) birestricts to the set of \(m\)-cells \(C_m\).

Proof

Follows directly from Lemma 4.3.

Lemma 4.5

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f, g \in C_m\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), if \(f\) and \(g\) are composable at dimension \(k\), then \(g \operatorname{\# }^k f\) is an \(m\)-cell in \(\mathsf{C}\).

Proof

Applying Axiom 2.3.2 and the fact that \(f\) and \(g\) are \(m\)-cells, we have that

\[ \operatorname{sc}^m (g \operatorname{\# }^k f) = \operatorname{sc}^m (g) \operatorname{\# }^k \operatorname{sc}^m (f) = g \operatorname{\# }^k f. \]
Corollary 4.6

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(k \in \mathcal{I}\) such that \(k {\lt} m\), the composition operation \(\operatorname{\# }^k\) birestricts to the set of \(m\)-cells \(C_m\).

Proof

Follows directly from Lemma 4.5.

Definition 4.7 Underlying single-sorted finite category

Let \(\mathsf{C}\) be a single-sorted \(n\)-category, and let \(m \in \mathbb {N}\) with \(m {\lt} n\). The underlying \(m\)-category of \(\mathsf{C}\) is the single-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) defined on the set of \(m\)-cells \(C_m\), with the source, target, and composition operations given by the birestrictions of those of \(\mathsf{C}\) to \(C_m\).

Proof

The birestrictions are well-defined by Corollaries 4.2, 4.4, and 4.6. Each axiom of single-sorted categories for \(\mathsf{C}^{{\lt}m}\) follows directly from the corresponding axiom for \(\mathsf{C}\).

Definition 4.8 Underlying single-sorted omega category

Let \(\mathsf{C}\) be a single-sorted \(\omega \)-category, and let \(m \in \mathbb {N}\). The underlying \(m\)-category of \(\mathsf{C}\) is the single-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) defined by the same construction as in Definition 4.7.

Proof

The single-sorted category axioms follow by the same argument as in Definition 4.7.

4.2 Underlying single-sorted functors

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(\mathcal{I}\)-categories, \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted functor, and \(m \in \mathcal{I}\). Then, for every \(f \in C_m\) we have that \(F(f) \in D_m\).

Proof

Applying Axiom 2.10.1 and the fact that \(f\) is an \(m\)-cell, we have that

\[ \operatorname{sc}^m (F(f)) = F(\operatorname{sc}^m (f)) = F(f). \]
Corollary 4.10

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(\mathcal{I}\)-categories, \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted functor, and \(m \in \mathcal{I}\). Then \(F\) birestricts to a function from \(C_m\) to \(D_m\).

Proof

Follows directly from Lemma 4.9.

Definition 4.11 Underlying 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 \(m {\lt} n\), the birestriction of \(F\) to the sets of \(m\)-cells defines a single-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\).

Proof

The birestriction is well-defined by Corollary 4.10. Each preservation axiom for \(F^{{\lt}m}\) follows directly from the corresponding axiom for \(F\).

Definition 4.12 Underlying single-sorted omega functor

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(\omega \)-categories, and let \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted \(\omega \)-functor. For any \(m \in \mathbb {N}\), the birestriction of \(F\) to the sets of \(m\)-cells defines a single-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\).

Proof

The argument is identical to that of Definition 4.11.

4.3 Single-sorted underlying functors

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

Definition 4.13 Single-sorted underlying functor

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

Proof

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