Coslice Colimits in Homotopy Type Theory

In this section, we explain the contributions of the paper along with its organization. We start by outlining the heart of the paper, which we call the main connection. Afterward, we describe three independent applications of the main connection in synthetic homotopy theory. Details, proofs, and related additional results are found in our associated technical report [6]. Further, we have formalized in Agda our construction of $A$-colimits as well as the universality of ordinary colimits for Corollary 21.

The HITs we consider are nonrecursive $2$-HITs, in the sense that they have only nonrecursive constructors of points and of paths of dimension one or two. Van Doorn et al. explicitly construct nonrecursive $2$-HITs in MLTT augmented with pushouts [28, Section 5]. When specialized to $A$-colimits, however, their construction has a significantly different form from ours and does not directly lead to the properties of $A$-colimits we derive. Moreover, they do not prove the full induction principle enjoyed by the $2$-HIT for their construction, whereas we do for ours. The full induction principle is necessary (and sufficient) to characterize the $2$-HIT uniquely.

Our work also builds on the theory of factorization systems. Such systems play important roles in model category theory [20], a key framework for classical homotopy theory. Moreover, in type theory, Rijke et al. have shown that factorization systems on $𝒰$ are closely connected to modalities [22], which are important in logic. We extend factorization systems to wild categories other than $𝒰$. Moreover, we lift factorization systems on $𝒰$ to wild categories of $𝒰$-valued diagrams (Lemma 22).

We assume the reader is familiar with MLTT and HITs in the style of [27]. We will work in MLTT augmented with ordinary colimits and denote this system by $\mathrm{𝖬𝖫𝖳𝖳}+\mathrm{𝖢𝗈𝗅𝗂𝗆}$. In fact, we need only augment MLTT with pushouts as they let us construct all nonrecursive $1$-HITs, including ordinary colimits, with all of their computational properties. Notably, $\mathrm{𝖬𝖫𝖳𝖳}+\mathrm{𝖢𝗈𝗅𝗂𝗆}$ comes with strong function extensionality for free. This property is critical for reasoning about functions in type theory and underlies our entire development (see, for example, Lemma 8). Overall, we carry out our proofs inside $\mathrm{𝖬𝖫𝖳𝖳}+\mathrm{𝖢𝗈𝗅𝗂𝗆}$ until Section 7. For Section 7 and Section 8, we also assume Voevodsky’s univalence axiom.

Before reviewing ordinary colimits, we recall two essential constructions in our type system. The first is the function $\mathrm{𝖺𝗉}:\left(x=y\right)\to \left(f(x)=f(y)\right)$ defined by path induction for all functions $f:X\to Y$ and $x,y:X$. (We use $=$ for the identity type and $\equiv$ for definitional equality.) If we view $X$ as an $\mathrm{\infty }$-groupoid, then $\mathrm{𝖺𝗉}$ is the action of $f$ on morphisms of $X$ (thereby exhibiting $f$ as a functor). The second is the transport function ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉}}^Y:{\prod }_{x,y:X}{\prod }_{p:x=y}Y(x)\to Y(y)$ for any type family $Y$ over $X$. This notion also gives us a dependent version of $\mathrm{𝖺𝗉}$: If $f:{\prod }_{x:X}Y(x)$, then we have a function ${\mathrm{𝖺𝗉𝖽}}_f:{\prod }_{x,y:X}{\prod }_{p:x=y}{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉}}^Y(p,f(x))=f(y)$. The transport function is essential for stating the induction principle for HITs, e.g., the colimits in Section 3.3. It also satisfies the following coherence law, which we need for our construction of $A$-colimits.

Finally, a remark on notation: we may use the Agda notation $(x:X)\to Y(x)$ for the type ${\prod }_{x:X}Y(x)$ for any type family $Y$ over $X$.

Let $𝒰$ be a universe and $A:𝒰$. In classical $1$-category theory, a diagram in a category $𝒞$ is a functor $F:ℐ\to 𝒞$, where $ℐ$ is the shape of the diagram. As long as $𝒞$ is cocomplete, we can form the functor ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{ℐ}$ sending each diagram over $ℐ$ to its colimit in $𝒞$. We, however, want the colimit of a diagram in the $\mathrm{\infty }$-category $A/𝒰$. This requires the diagram to be an $\mathrm{\infty }$-functor: the functor laws must satisfy coherence laws up to homotopy, which themselves must satisfy higher coherence laws, and so on at arbitrarily high levels. It is unknown whether such $\mathrm{\infty }$-functors are definable in HoTT.

To avoid infinite coherence conditions, we specialize $ℐ$ to the free category generated by a graph. A graph $\mathrm{\Gamma }$ is a pair $({\mathrm{\Gamma }}_0,{\mathrm{\Gamma }}_1)$ consisting of a type ${\mathrm{\Gamma }}_0:𝒰$ of vertices and a family ${\mathrm{\Gamma }}_1:{\mathrm{\Gamma }}_0\to {\mathrm{\Gamma }}_0\to 𝒰$ of edges. A $\mathrm{\Gamma }$-shaped diagram $F$ in $A/𝒰$ is a pair $(F_0,F_1)$ consisting of a function $F_0:{\mathrm{\Gamma }}_0\to A/𝒰$ and a family of maps $F_1:(i,j:{\mathrm{\Gamma }}_0)\to {\mathrm{\Gamma }}_1(i,j)\to F_0(i){\to }_A{F}_0(j)$. We may write $F$ for $F_0$ and $F_1$. The induced diagram in $A/𝒰$ satisfies all the infinite coherence laws because its domain is freely generated by the points and edges of $\mathrm{\Gamma }$.

We will see that $A$-colimits interact nicely with trees. A tree is a graph without non-directed cycles. Formally, a graph $\mathrm{\Gamma }$ is a tree if the quotient ${\mathrm{\Gamma }}_0/{\mathrm{\Gamma }}_1$ is contractible. Both $\mathbb{N}$ and $\mathbb{Z}$ are trees when equipped with the successor ordering:

Another example of a tree is a span $\bullet \leftarrow \bullet \to \bullet$, on which pushouts are defined.

Rijke has defined the notion of directed tree and has defined an interpretation function sending an element of a $𝖶$-type to a directed tree [23, The underlying trees of elements of W-types]. Intuitively, a directed tree is a rooted graph such that for each vertex $v$, there is a single directed path (including the trivial path) from $v$ to the root. Every directed tree is a tree in our sense [6, Corollary 4.0.6]. Thus, elements of a $𝖶$-type can be realized as trees.

Let $F$ be a $\mathrm{\Gamma }$-shaped diagram in $𝒰$. The (ordinary) colimit of $F$ is the HIT ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(F)$ generated by

These two constructors make ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(F)$ a cocone under $F$ (or $F$-cocone): a type $C$ equipped with maps $u:{\prod }_{i:{\mathrm{\Gamma }}_0}{F}_i\to C$ and homotopies $K:{\prod }_{i,j,g}{u}_j\circ F_{i,j,g}\sim u_i$. What characterizes ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(F)$ as a colimit of $F$ is that $\kappa$ is a (homotopy) initial $F$-cocone [24]. Equivalently, for every $X:𝒰$, the function

is an equivalence, where ${\mathrm{𝖢𝗈𝖼𝗈𝗇𝖾}}_F(X)$ denotes the type of $F$-cocones on $X$.

Our proof of Theorem 15 will use the induction principle for ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(F)$. This states that for every type family $E$ over ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(F)$ together with data

we have a function $\mathrm{𝗂𝗇𝖽}(E,r,R):{\prod }_{z:{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(F)}E(z)$ that satisfies $\mathrm{𝗂𝗇𝖽}(E,r,R)({\iota }_i(x))\equiv r(i,x)$ and is equipped with an identity ${\rho }_{\mathrm{𝗂𝗇𝖽}(E,r,R)}(i,j,g,x):{\mathrm{𝖺𝗉𝖽}}_{\mathrm{𝗂𝗇𝖽}(E,r,R)}({\kappa }_{i,j,g}(x))=R(i,j,g,x)$.

We now introduce (orthogonal) factorization systems on wild categories. For us, the key property of such systems is that they interact nicely with adjunctions. In Section 7, we deduce from this property, combined with the main connection, that $A$-colimits preserve the left classes of factorization systems on $𝒰$.

For the next lemma, where $𝒞$ is a univalent bicategory, $𝒞$ is similar enough to $𝒰$ that the proof of the lemma for $𝒰$ can be transferred to $𝒞$.⁴⁴4For the proof of this lemma for $𝒰$, see [22, Lemma 1.46]. Indeed, univalence lets us characterize the identity types of ${\mathrm{𝖿𝖺𝖼𝗍}}_{ℒ,ℛ}(h)$ via the fundamental theorem of identity types [21, Theorem 11.2.2]. Moreover, Lemma 5 gives us a suitable diagonal filler for the key commuting square used by the proof. Before stating the next lemma, we need a definition.

This alternative definition of $ℒ$ is useful for the proof of Theorem 13, below. For this theorem, we need to introduce adjoint pairs of functors between wild categories.

We can generalize ordinary colimits in Section 3 to all coslices $A/𝒰$. For each $Y:\mathrm{𝖮𝖻}(A/𝒰)$, an $F$-cocone on $Y$ consists of a family of maps $h:(i:{\mathrm{\Gamma }}_0)\to F_i{\to }_{A}Y$ in $A/𝒰$ together with an identity $H_{i,j,g}:h_j\circ F_{i,j,g}=h_i$ for all $i,j:{\mathrm{\Gamma }}_0$ and $g:{\mathrm{\Gamma }}_1(i,j)$. In this situation, we say that $Y$ is a colimit of $F$ if $(h,H)$ is initial in the category of $F$-cocones. This means that for each $X:\mathrm{𝖮𝖻}(A/𝒰)$, the function

is an equivalence. We must include the associativity term since associativity of maps does not hold judgmentally in $A/𝒰$ (whereas it does in $𝒰$).

Observe that by a variant of Lemma 8, $h_j\circ F_{i,j,g}=h_i$ is equivalent to the type of homotopies ${\eta }_{i,j,g}:\mathrm{𝖿𝗎𝗇}(h_j)\circ \mathrm{𝖿𝗎𝗇}(F_{i,j,g})\sim \mathrm{𝖿𝗎𝗇}(h_i)$ equipped with a commuting square

of paths for each $a:A$. It is this family of $2$-cells which distinguishes the colimit of $F$, in $A/𝒰$, from ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$. Here, we reuse $ℱ$ to denote the evident forgetful functor from $\mathrm{\Gamma }$-shaped diagrams in $A/𝒰$ to those in $𝒰$. The $2$-cells affect ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$ by collapsing its nontrivial loops formed by paths of the form $\eta (\mathrm{𝗌𝗍𝗋}(F_i)(a))$. We call such loops distinguished loops in ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$. For example, if $i\equiv j$ and $F_{i,j,g}\equiv {\mathrm{𝗂𝖽}}_{F_i}$, then (5.1) is equivalent to $\eta (\mathrm{𝗌𝗍𝗋}(F_i)(a))={\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖿𝗎𝗇}(h_i)(\mathrm{𝗌𝗍𝗋}(F_i)(a))}$. In this case, it fills the loop $\eta (\mathrm{𝗌𝗍𝗋}(F_i)(a))$.

If our setting behaved like the classical one, the colimit of $F$ in $A/𝒰$ would arise as the ordinary colimit of the augmented diagram: $ℱ(F)$ augmented with the canonical arrow from $A$ to $ℱ(F_i)$ for each $i:{\mathrm{\Gamma }}_0$ [17, Proposition 4.6]. If $\mathrm{\Gamma }$ is discrete, i.e., ${\mathrm{\Gamma }}_1$ is the empty relation, then the $A$-colimit of $F$ inside HoTT is, in fact, the colimit of

In general, though, this construction is wrong inside HoTT. For example, the pointed colimit of the diagram $\mathrm{𝟏}\stackrel{𝗂𝖽}{\to }\mathrm{𝟏}$ is trivial, but the colimit of the augmented diagram

is the circle $S^1$. The reason for the discrepancy between the classical case and ours is that unless $\mathrm{\Gamma }$ is discrete, the augmented diagram inside HoTT adds arrows that are intended as composites but are not interpreted as such in the model of HoTT. Rather, the model sees them as freely added to the diagram.

Our approach to building the colimit of $F$ never creates an augmented diagram, thereby avoiding the problem of Section 5.2. We start with the ordinary colimit ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$ which ignores the coslice structure of $F$. Then, we glue onto this colimit the $2$-cells required by the coslice colimit. We do this via a quotient of ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$ that fills its distinguished loops.

To this end, define ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}A\stackrel{𝜓}{\to }{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$ by colimit induction, as the function induced by the cocone

under the constant diagram at $A$. The homotopy $W:{\iota }_j\circ \mathrm{𝗌𝗍𝗋}(F_j)\sim {\iota }_i\circ \mathrm{𝗌𝗍𝗋}(F_i)$ is defined by $W(a)≔{\mathrm{𝖺𝗉}}_{{\iota }_j}{(\mathrm{𝗉𝗍}(F_{i,j,g})(a))}^{-1}\cdot {\kappa }_{i,j,g}(\mathrm{𝗌𝗍𝗋}(F_i)(a))$. Intutively, $\psi$ finds the distinguished loops of ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$. Next, form the pushout square

which, by the definition of pushout types, comes with a homotopy ${\mathrm{𝗀𝗅𝗎𝖾}}_{{𝒫}_F}:\mathrm{𝗂𝗇𝗅}\circ \left[{\mathrm{𝗂𝖽}}_A\right]\sim \mathrm{𝗂𝗇𝗋}\circ \psi$. This pushout is our approach to forming the desired quotient of ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))$.

Back to the general case, with the equivalence $⟨-,-⟩$ of Lemma 8, we can form an $F$-cocone on $({𝒫}_F,\mathrm{𝗂𝗇𝗅})$

as follows. We have a homotopy ${\delta }_{i,j,g}≔\lambda (x:\mathrm{𝗍𝗒}(F_i)).{\mathrm{𝖺𝗉}}_{\mathrm{𝗂𝗇𝗋}}({\kappa }_{i,j,g}(x))$ from $\mathrm{𝗂𝗇𝗋}\circ {\iota }_j\circ \mathrm{𝖿𝗎𝗇}(F_{i,j,g})$ to $\mathrm{𝗂𝗇𝗋}\circ {\iota }_i$. Further, for each $a:A$, we have a chain ${ϵ}_{i,j,g}(a)$ of identities

Let $𝒦({𝒫}_F)$ denote this $F$-cocone structure on $({𝒫}_F,\mathrm{𝗂𝗇𝗅})$.

So far, we have defined a function ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A≔𝒫:\mathrm{𝖮𝖻}(\mathrm{𝖣𝗂𝖺𝗀}(\mathrm{\Gamma },A/𝒰))\to \mathrm{𝖮𝖻}(A/𝒰)$ sending a $\mathrm{\Gamma }$-shaped diagram in $A/𝒰$ to its $A$-colimit. We now make $𝒫$ a functor by describing its action on maps of diagrams. We want to describe this action in terms of the action of the ordinary colimit functor by using the special form of $𝒫$’s object function. Moreover, we must verify that such a description is correct by proving that $𝒫$ is left adjoint to the constant diagram functor, i.e., enjoys the universal property of the colimit functor.

Suppose that $F$ and $G$ are $\mathrm{\Gamma }$-shaped diagrams in $A/𝒰$. The type of natural transformations from $F$ to $G$ consists of families $d:(i:{\mathrm{\Gamma }}_0)\to \mathrm{𝗍𝗒}(F_i){\to }_A\mathrm{𝗍𝗒}(G_i)$ of maps equipped with an $A$-homotopy $G_{i,j,g}\circ d_i{\sim }_A{d}_j\circ F_{i,j,g}$ for all $i,j,g$, where ${\sim }_A$ is as in Lemma 8. Consider a natural transformation $\delta ≔(d,⟨\xi ,\tilde{\xi }⟩)$

from $F$ to $G$, where $⟨-,-⟩$ is as in Lemma 8. We form a map ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(\delta ):{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(F){\to }_A{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(G)$ as follows. Start with the function ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(F))\stackrel{\overline{\delta }}{\to }{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}(ℱ(G))$ induced by the following map of $𝒰$-valued diagrams over $\mathrm{\Gamma }$:

Note that for each $a:A$,

We may assume that ${\tilde{\xi }}_{i,j,g}(a)$ instead has the equivalent type

Here we abbreviate the right endpoint of the path by $E_{i,j,g}(a)$. Now, the triangle

commutes by induction on ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}A$. Indeed, the computation rules of these functions give us

for all $i:{\mathrm{\Gamma }}_0$ and $a:A$. Further, by defining ${\mathrm{\Lambda }}_{i,j,g}(a)≔C_j(a)\cdot {\mathrm{𝖺𝗉}}_{{\psi }_G}({\kappa }_{i,j,g}(a))$, we have a chain of identities

for all $i,j:{\mathrm{\Gamma }}_0$, $g:{\mathrm{\Gamma }}_1(i,j)$, and $a:A$, so (5.4) commutes. We now have a map

of spans, which induces a function ${\mathrm{\Psi }}_{\delta }:{𝒫}_F\to {𝒫}_G$ by the universal property of pushouts. Since ${\mathrm{\Psi }}_{\delta }(\mathrm{𝗂𝗇𝗅}(a))\equiv \mathrm{𝗂𝗇𝗅}(a)$ for all $a:A$, we may take ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(\delta )$ as $({\mathrm{\Psi }}_{\delta },\lambda a.{\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝗂𝗇𝗅}(a)}):{𝒫}_F{\to }_A{𝒫}_G$.

To verify that the functor $\mathrm{𝖣𝗂𝖺𝗀}(\mathrm{\Gamma },A/𝒰)\stackrel{{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A}{\to }A/𝒰$ we’ve defined is correct, we must show that it is left adjoint to the constant diagram functor. To do so, we construct the terms ${𝗇}_1$ and ${𝗇}_2$ required by Definition 12.

The two lower horizontal functions are induced by post-composition with $s$ and pre-composition with $\delta$ [6, Definition 5.4.11], respectively.

Lemma 16 is a routine computation, whereas Lemma 17 is quite difficult. The proof of Lemma 17 is easier for the map ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(F){\to }_A{\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(G)$ obtained by applying the inverse of $\mathrm{𝗉𝗈𝗌𝗍𝖼𝗈𝗆𝗉}(𝒦({𝒫}_F),{𝒫}_G,\mathrm{𝗂𝗇𝗅})$ to the canonical $F$-cocone on ${𝒫}_G$ induced by $\delta$. Therefore, we decide to reduce the goal to an equality between this map and ${\mathrm{𝖼𝗈𝗅𝗂𝗆}}_{\mathrm{\Gamma }}^A(\delta )$. We achieve this by showing that they belong to the same fiber of $\mathrm{𝗉𝗈𝗌𝗍𝖼𝗈𝗆𝗉}(𝒦({𝒫}_F),{𝒫}_G,\mathrm{𝗂𝗇𝗅})$, which is contractible by Theorem 15. Though much easier than a direct approach to Lemma 17, this method requires intricate computations. We have formalized both Lemma 16 and Lemma 17 (see [7, Colimit-code/Map-Nat/CosColimitPstCmp.agda] and [7, Colimit-code/Map-Nat/CosColimitPreCmp.agda], respectively).