Formalizing Colimits in $𝒞\text{at}$

The fact that the “homotopy category $⊣$ nerve” adjunction can be constructed as a composite of two other adjunctions follows from the fact that the nerve functor factors (up to isomorphism) as a composite of two right adjoints, through a category that we now introduce. Recall that the category of simplicial sets is defined as a presheaf category $𝒮{\text{et}}^{{\mathrm{\Delta }}^{\text{op}}}$. Given $n:\mathbb{N}$, we define the $n$-truncated simplex category ${\mathrm{\Delta }}_{\le n}$ as the full subcategory ${\mathrm{\Delta }}_{\le n}\subset \mathrm{\Delta }$ spanned by the objects $[0],\mathrm{\dots },[n]$. The category of $n$-truncated simplicial sets, $𝒮{\text{et}}^{{\mathrm{\Delta }}_{\le n}^{\text{op}}}$, is then the category of presheaves over ${\mathrm{\Delta }}_{\le n}$. The restriction functor, known as $n$-truncation, has fully faithful left and right adjoints defined by left and right Kan extension:⁸⁸8The right and left Kan extensions exist because $\mathrm{\Delta }$ is small and $𝒮\text{et}$ is complete and cocomplete.

For any functor valued in simplicial sets, we can obtain its $n$-truncated version by postcomposing with the functor ${\text{tr}}_n:𝒮{\text{et}}^{{\mathrm{\Delta }}^{\text{op}}}\to 𝒮{\text{et}}^{{\mathrm{\Delta }}_{\le n}^{\text{op}}}$. In particular, the 2-truncated nerve ${\text{nerve}}_2$ is defined to be the composite functor:

The canonical natural transformation $\upsilon :\text{nerve}\Rightarrow {\text{cosk}}_2{\text{nerve}}_2$ is defined by left whiskering the unit $\eta :\text{id}\Rightarrow {\text{cosk}}_2{\text{tr}}_2$ of the adjunction ${\text{tr}}_2⊣{\text{cosk}}_2$ with the nerve functor:

The natural transformation $\upsilon$ is the underlying map of the isomorphism Nerve.cosk₂Iso.

A simplicial set $X$ is 2-coskeletal just when the unit component ${\eta }_X:X\to {\text{cosk}}_2{\text{tr}}_{2}X$ is an isomorphism. Thus, our first main subproblem, to prove that the natural transformation $\upsilon$ is a natural isomorphism, is achieved by the following proposition:

We unpack the 2-coskeletality condition and describe the proof of Proposition 6 in §3.5.

On account of the natural isomorphism $\upsilon :\text{nerve}\cong {\text{cosk}}_2{\text{nerve}}_2$ provided by Proposition 6, it now suffices to construct a left adjoint ${\text{ho}}_2:𝒮{\text{et}}^{{\mathrm{\Delta }}_{\le 2}^{\text{op}}}\to 𝒞\text{at}$ to the functor ${\text{nerve}}_2$. To do so, we unpack the data contained in a (2-truncated) simplicial set.

On paper there is a well-known presentation of the morphisms in the SimplexCategory $\mathrm{\Delta }$ by generators and relations [11, §I.1] that is in the process of being formalized by Robin Carlier. At present, mathlib contains the generating face maps ${\delta }^i:[n]\to [n+1]$, corresponding to monomorphisms whose image omits $i\in \text{Fin}(n+2)$, as well as the generating degeneracy maps ${\sigma }^i:[n+1]\to [n]$, corresponding to epimorphisms for which $i\in \text{Fin}(n+1)$ has two elements in its preimage; mathlib also knows the composition relations these maps satisfy, but does not contain a proof that $\mathrm{\Delta }$ is equivalent to the category SimplexCategoryGenRel with this presentation.

A 2-truncated simplicial set $X$ is given by the data of three sets $X_0,X_1,X_2$ and maps between them indexed by the morphisms between the three objects $[0],[1],[2]:{\mathrm{\Delta }}_{\le 2}\subset \mathrm{\Delta }$. The further 1-truncation of $X$ is given by the data below-left defined by the contravariant actions of the morphisms in ${\mathrm{\Delta }}_{\le 1}$ displayed below-right:

The composition relations ${\sigma }^0\circ {\delta }^0=\text{id}={\sigma }^0\circ {\delta }^1$ in $\mathrm{\Delta }$ induce dual relations ${\delta }_0\circ {\sigma }_0=\text{id}={\delta }_1\circ {\sigma }_0$. As explained in Example 11, this is closely related to categorical data known as a reflexive quiver.

A quiver is defined in mathlib as a type equipped with a dependent type of arrows:

Kim Morrison formalized the “free $⊣$ forgetful” adjunction between the category $𝒬\text{uiv}$, of quivers and structure-preserving morphisms, called prefunctors, between them, and $𝒞\text{at}$.

A similar result also holds for reflexive quivers, which extend quivers with specified “identity” endo-arrows for each term in the base type:

We introduced reflexive quivers and reflexive prefunctors and defined the evident forgetful functors $U^r:𝒞\text{at}\to \text{r}𝒬\text{uiv}$ from the category of categories to the category of reflexive quivers and $U^q:\text{r}𝒬\text{uiv}\to 𝒬\text{uiv}$ from the category of reflexive quivers to the category of quivers. Definitionally, we have $U=U^q{U}^r:𝒞\text{at}\to 𝒬\text{uiv}$.

This defines a functor $F^r:\text{r}𝒬\text{uiv}\to 𝒞\text{at}$ and a natural transformation $q:F{U}^q\Rightarrow F^r$ whose components $q_Q:F{U}^{q}Q\to F^{r}Q$ are universal among functors with domain $F{U}^{q}Q$ that respect the hom relation, sending the specified reflexivity arrows of $Q$ to identities.

We then formalized the following proof:

In mathlib, many notions come in two flavors of presentation, referred to as the “bundled” and “(partially) unbundled” presentations.¹⁰¹⁰10There is also a “fully unbundled” presentation, but mathlib does not use it and we will not discuss it. In the unbundled presentation, a category is given as a type variable $C$ together with a typeclass instance argument Category $C$ which provides the rest of the data for a category whose type of objects is $C$. This allows for a form of formal synecdoche, where one need only explicitly mention the type of objects and the rest of the structure comes along for the ride. In bundled style a category is an element $C:\text{Cat}$, with suitable projections $\text{ob}C:\mathrm{𝖳𝗒𝗉𝖾}$ and $\text{Hom}:\text{ob}C\to \text{ob}C\to \mathrm{𝖳𝗒𝗉𝖾}$.

Generally, mathlib prefers the unbundled form, but the bundled form is necessary if we need to consider the category of categories, that is, Category Cat, and our main theorem is about Cat so we cannot avoid it completely. A similar situation occurs for functors, which appear unbundled as $C\rightharpoonup \rightharpoondown D$ and also bundled as ${\text{Hom}}_{\text{Cat}}(C,D)$.¹¹¹¹11Note the former notion of functor is strictly speaking more general than the latter, in which the universe levels of the domain category must match those of the codomain. There is functor composition $F⋙G$ and morphism composition $F{\gg }_{\text{Cat}}G$, and so on. Not only are many notions duplicated, but by applying lemmas coming from each context one can end up with a mixture of both notions in goals, and simplification would frequently get stuck in this situation. We eventually mitigated this issue by unbundling as early as possible, stating lemmas only in the unbundled form, and packaging them up only for the higher order statements about operations on Cat.

Our main theorem fundamentally deals with the 1-categorical (rather than 2-categorical) structure of $𝒞\text{at}$. The very statement that $𝒞\text{at}$ has small colimits involves equality of functors, as does the definition of the nerve – a simplicial set rather than a simplicially-indexed category-valued pseudofunctor.¹²¹²12The nerve of $C$ could be regarded as a pseudofunctor $\text{nerve}C:{\mathrm{\Delta }}^{\text{op}}\to 𝒞\text{at}$ valued in $𝒞\text{at}$, sending the object $[n]:\mathrm{\Delta }$ to the category of functors $\text{Fin}(n+1)\to C$, but this extra coherence data is unnecessary. The type-valued mapping $\text{nerve}C:{\mathrm{\Delta }}^{\text{op}}\to 𝒮\text{et}$ is strictly functorial, and indeed (due to the care taken in formalizing the definition of ComposableArrows) the map_id and map_comp fields of nerve are filled by rfl. There are advantages to working strictly (1-categorically) rather than weakly (2-categorically or bicategorically) when possible. In future work, described in §5, we plan to use our homotopy category functor to convert from simplicial to categorical enrichments. As we have formalized this as a strict functor between 1-categories we can tap into existing mathlib developments of change of base in enriched category theory.

Lean’s mathlib provides an extensionality theorem for functors, contributed by Reid Barton, but note the warning:

So we knew in advance there would be trouble coming and needed to structure our proofs in specific ways to take advantage of eqToHom.

At the core of this warning is the following issue: When one has an equality of objects, or an equality of functors (which involves an equality of objects – the h_obj assumption above), this induces an equality of types, namely $\text{Hom}(A,B)=\text{Hom}(A,B^{\prime })$ given $B=B^{\prime }$. In dependent type theory, if one has $f:\text{Hom}(A,B)$ and an equality $h:B=B^{\prime }$, the plain expression $f:\text{Hom}(A,B^{\prime })$ does not typecheck (unless $B$ and $B^{\prime }$ are definitionally equal). However, it is possible to use $h$ to cast $f$ to the correct type, producing a term $\text{cast}hf:\text{Hom}(A,B^{\prime })$. This is also known as “rewriting” and it is a common technique in proofs (using the rw tactic), but it is hazardous when applied to “data” such as $f$, because $\text{cast}hf$ is not the same term as $f$ and so mismatches can arise between expressions such as $\text{cast}h(f\circ g)$ and $(\text{cast}hf)\circ g$. It is possible to prove these are equal, but it generally requires a rather delicate “induction on equality” to prove, with a manually written induction motive. Complications with transport of this nature are often referred to as “DTT hell.”

The mathlib statement of Functor.ext is employing a technique to avoid this issue, which is to make use of the category structure to help alleviate the pains associated with using the cast function directly, by first converting $h:B=B^{\prime }$ into $\text{eqToHom}h:\text{Hom}(B,B^{\prime })$, so that $(\text{eqToHom}h)\circ f:\text{Hom}(A,B^{\prime })$. This presents the casting of $f$ as a composition, which means that many more lemmas from category theory apply (such as associativity of composition), and eqToHom itself has many lemmas for how it factors over various operations.

For the most part, this technique did its job. Although we obtained many goals that involved these eqToHom morphisms, after formalizing appropriate lemmas, the simplifier was able to push them out of the way. For instance, we added a Quiver.homOfEq to perform an analogous casting for (reflexive) quivers (which lack composition) and proved various lemmas by induction on equality. This is the kind of complication that essentially never appears in informal category theory, due to its more extensional handling of morphism typing.

Another example of DTT hell arises in the proof of nerveFunctor₂.full, that the 2-truncated nerve functor ${\text{nerve}}_2:𝒞\text{at}\to 𝒮{\text{et}}^{{\mathrm{\Delta }}_{\le 2}^{\text{op}}}$ is full. Given a pair of categories $C$ and $D$ and a map $F:{\text{nerve}}_{2}C\to {\text{nerve}}_{2}D$ between their 2-truncated nerves, our task is to lift this to a functor between $C$ and $D$. The underlying reflexive prefunctor is defined by the 1-truncation of $F$, but it remains to show that this reflexive prefunctor is functorial, preserving composition of morphisms in $C$ in addition to identities.

The idea of the proof is to note that the composable morphisms $k\circ h$ define a 2-simplex ${\sigma }_{k,h}:{({\text{nerve}}_{2}C)}_2$. The 2-simplex $F({\sigma }_{k,h}):{({\text{nerve}}_{2}D)}_2$ defines a functor $\text{Fin}(3)\to D$, which gives rise to a commutative triangle involving three arrows in $D$. Using the naturality of $F$ with respect to the three morphisms ${\delta }^i:[1]\to [2]$, this may be converted into the desired equality $F(k\circ h)=Fk\circ Fh$. But these naturality equalities live in the type ${({\text{nerve}}_{2}D)}_1$ of functors $\text{Fin}(2)\to D$, which give rise to heterogeneous equalities between the corresponding arrows in $D$. We were forced to first prove and then string together a sequence of heterogeneous equalities before finally concluding the desired equality between arrows belonging to the same hom-type. It then remained to show that the 2-truncated nerve carries this lifted functor to the original map $F$, which is proven using Proposition 13(ii).

In Proposition 13(i), our aim is to define a map of 2-truncated simplicial sets $F:X\to {\text{nerve}}_{2}C$ from a map between the underlying reflexive quivers. Such a map is a natural transformation with three components $F_0$, $F_1$, and $F_2$ corresponding to the three objects $[0],[1],[2]:{\mathrm{\Delta }}_{\le 2}$, which can be constructed straightforwardly from the hypotheses. But complications arise in the proof of naturality, which amounts to establishing commutative squares of the form

for each morphism $\alpha :[m]\to [n]$ in ${\mathrm{\Delta }}_{\le 2}$ (there are 31 such morphisms). One annoyance, discussed at the start of §2.2, is the fact that mathlib does not yet know that ${\mathrm{\Delta }}_{\le 2}$ is generated by the three degeneracy maps ${\sigma }^i$ and the five face maps ${\delta }^i$. Our initial formalization instead explicitly treated the nine cases presented by the choice of domain and codomain objects, with the cases involving a morphism with domain $[2]$ reducing to the cases involving domain $[0]$ or $[1]$ by the 2-coskeletality of the nerve. Once we fixed domain and codomain objects there were often further case splits involving the specific nature of the morphism $\alpha :[m]\to [n]$.

When we submitted this as a pull request to mathlib, the reviewer Joël Riou suggested we think of this result as the task of showing that the MorphismProperty of satisfying the naturality condition (17) holds for every morphism $\alpha$ in ${\mathrm{\Delta }}_{\le 2}$. An easier task than showing that the simplex category can be presented by generators and relations is to show that the naturalityProperty of its arrows follows from the cases corresponding to faces and degeneracy maps, as Riou formalized for us in Truncated.morphismProperty_eq_top. This reduces the problem to the eight cases corresponding to generating morphisms $\alpha :[m]\to [n]$ in ${\mathrm{\Delta }}_{\le 2}$, each of which still involves establishing an equality between functors $\text{Fin}(m+1)\to C$.

The extensionality result of Proposition 13(ii) is simpler but still less innocuous than it appears. Two natural transformations $F$ and $G$ are equal just when their three components are equal, and as these are functions between types it suffices to show they define the same mapping on terms. However, this involves proving equalities in the types ${({\text{nerve}}_{2}C)}_0$, ${({\text{nerve}}_{2}C)}_1$, and ${({\text{nerve}}_{2}C)}_2$, which are types of functors, and thus these equalities involved a fair amount of pain. In the final case $F_2=G_2$, naturality again provided us with equalities in the type ${({\text{nerve}}_{2}C)}_1$ of functors $\text{Fin}(2)\to C$ which gave rise to heterogeneous equalities between the mappings on arrows of the functors $\text{Fin}(3)\to C$ we were tasked with identifying.

By a folklore result involving Reedy category theory [31], a simplicial set $X$ is $2$-coskeletal, meaning that the adjunction unit component ${\eta }_X:X\to {\text{cosk}}_2{\text{tr}}_{2}X$ is an isomorphism, just when every $k$-simplex boundary in $X$ can be filled to a simplex, for all $k>2$. This property would be easy to check in the case where $X$ is the nerve of a category, but unfortunately this characterization of 2-coskeletal simplicial sets has not been formalized. Thus, we directly unpack the invertible unit component definition into a condition that we can actually check.

Recall the functor ${\text{cosk}}_2$ is defined by right Kan extension along the inclusion ${\mathrm{\Delta }}_{\le 2}^{\text{op}}\hookrightarrow {\mathrm{\Delta }}^{\text{op}}$. Thus, the condition of a simplicial set $X$ being 2-coskeletal asserts that the identity natural transformation defines a right Kan extension:

As the category $𝒮\text{et}$ is complete, any such right Kan extension (18) is pointwise, meaning that $X$ is 2-coskeletal if and only if for each $n:\mathbb{N}$, a canonical cone – with summit $X_n$ over a diagram with objects $X_j$ indexed by arrows $[j]\to [n]$ in $\mathrm{\Delta }$ with $j\le 2$ – is a limit cone, the definition of which we now recall:

Thus, for the simplicial set $\text{nerve}C$, we must:

1. (i)

   Construct lift, a function valued in functors $\text{Fin}(n+1)\to C$.

2. (ii)

   Prove fac, an equality between functions valued in functors $\text{Fin}(j+1)\to C$ for $j=0,1,2$.

3. (iii)

   Prove uniq, an equality between functions valued in functors $\text{Fin}(n+1)\to C$.

We submitted a proof along these lines in our initial mathlib pull request, involving repeated painful appeals to Functor.ext. During the PR review process, Joël Riou suggested a useful abstraction boundary, using the following characterization of simplicial sets defined by nerves of categories.

As Proposition 19 explains, the only examples of strict Segal simplicial sets are nerves of categories. But it was cleaner to formalize the proof that a strict Segal simplicial set $X$ is 2-coskeletal because the functions involved in lift, fac, and uniq are now valued in an abstract type $X_n$ which is equivalent to the type of paths of edges of length $n$ in $X$. Thus, we formalized:

together with a proof Nerve.strictSegal of the implication (i)$\Rightarrow$(ii) in Proposition 19.