On Left Adjoints Preserving Colimits in HoTT

In category theory, a basic and eminently useful fact is that left adjoints preserve colimits (LAPC). We would like to invoke this classical theorem in the categorical setting of synthetic homotopy theory, the axiomatic and usually type-theoretic study of topological spaces with higher-dimensional structure. This would let us produce new universal constructions of spaces from existing ones via purely algebraic methods. For synthetic homotopy theory carried out in homotopy type theory (HoTT), the appropriate categorical setting is that of wild categories, the canonical examples of which are type universes. This notion is a type-theoretic approximation of an $(\mathrm{\infty },1)$-category that specifies the data of a $1$-category but omits higher coherence data. Despite its naivete, this setting is expressive enough to study concepts like (co)limits and adjunctions inside type theory.

We would like to port LAPC to adjunctions between wild categories. In particular, we would like to port the “standard” proof, i.e., the proof one would expect to see based on the category theory literature. This, however, turns out to be harder than one might hope as we produce, inside HoTT, an example of such an adjunction for which the proof fails. Nevertheless, we identify a sufficient condition for the proof to go through. Roughly, it expresses that the adjunction data interacts nicely with the left adjoint’s (proof-relevant) composition law. With this condition, combined with a higher version a known technique based on homogeneous types, we show that suspension, an example of a left adjoint, preserves (graph-indexed) colimits, which has applications to the theory of acylic types and to homology theory. We also show that every modality (such as truncation), viewed as a functor on coslices of a type universe, satisfies the condition as a left adjoint to the forgetful functor. As a result, the full wild subcategory of modal types inherits colimits from the ambient coslice. Our proof of this fact differs from the one described for truncations by [26, Section 7.4]. Ours is ultimately simpler by placing modalities in the general context of left adjoints.

The sufficient condition for the standard proof and its application to truncations were mentioned briefly in prior work by Hart and Favonia [12, Remark 24]. In the present work, we place these results in a wider context and explain, for the first time, how one proves them. Moreover, we have formalized all our main results in Agda.

We review some basic constructions in HoTT that are important for our work. We assume the reader is familiar with Martin-Löf type theory (MLTT), the core type system of HoTT, in the style of [26]. Notably, MLTT is sufficient for the core of our work: all of Section 5 is carried out in MLTT (with function extensionality). For Sections 6 and 7, we postulate a simple class of HITs: pushout types [26, Section 6.8]. In particular, Section 6 focuses on suspensions, a kind of pushout.

In this section, we record essential concepts and constructions in wild category theory, including adjunctions. The reader will notice that the basic definitions are naive translations of their classical counterparts.

The key distinction between wild categories and the categories of [26, Section 9.1] is that the latter have hom types that behave as sets, i.e., have trivial identity types, so that all higher coherences between morphisms in them hold trivially. By contrast, wild categories simply ignore such coherences. In synthetic homotopy theory, many wild categories have hom types that are not sets, so developing the theory of wild categories is worthwhile.

The following notion generalizes the univalence axiom [26, Axiom 2.10.3] and can significantly simplify proofs. We will invoke it in the proof of Corollary 23.

For each adjunction $L⊣R$, we also have naturality squares

Here, the right-hand square is defined by the commuting square

where ${\eta }_{\psi }$ and ${ϵ}_{\psi }$ are from the equivalence data of $\psi$. The left-hand square is defined similarly.

In particular, $({\psi }^{-1},{\widetilde{\mathrm{𝗇𝖺𝗍}}}_{\text{dom}})$ is a natural isomorphism ${\mathrm{𝗁𝗈𝗆}}_{𝒞}(-,R(Y))\Rightarrow {\mathrm{𝗁𝗈𝗆}}_{𝒟}(L(-),Y)$ for each $Y:\mathrm{𝖮𝖻}(𝒟)$. The terms ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}$ and ${\widetilde{\mathrm{𝗇𝖺𝗍}}}_{\text{dom}}$ are related by the following exchange law.

This section is the core of the paper. We find a sufficient, practically useful condition for the standard proof of LAPC to work for wild categories. Informally, the condition states that ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}$ interacts nicely with the composition law of the left adjoint.

Let $𝒞$ be a wild category. Let $\mathrm{\Gamma }$ be a graph and $F:\mathrm{\Gamma }\to 𝒞$ be a $𝒞$-valued diagram over $\mathrm{\Gamma }$. Consider a cocone $𝒦≔(C,r,K)$ under $F$, where $r_i:F_i\to C$ for each $i:{\mathrm{\Gamma }}_0$ and $K_{i,j,g}:r_j\circ F_{i,j,g}=r_i$ for all $i,j:{\mathrm{\Gamma }}_0$ and $g:{\mathrm{\Gamma }}_1(i,j)$.

Definition 10 expresses that for every cocone ${𝒦}^{\prime }$ under $F$, there is a unique cocone morphism $𝒦\to {𝒦}^{\prime }$. Let $𝒟$ be a wild category and $L:𝒞\to 𝒟$ be a functor. We have an induced diagram $L(F)$ and an induced cocone $L(𝒦)$ under $L(F)$:

Suppose that $𝒦$ is colimiting and that we have an adjunction $(\psi ,{\mathrm{𝗇𝖺𝗍}}_{\text{cod}},{\mathrm{𝗇𝖺𝗍}}_{\text{dom}}):L⊣R$. We wish to replay the standard classical proof by showing the chain of isomorphisms (1.1) equals the post-composition map. Let us preview this argument. Let $\zeta$ denote the composite of the isomorphisms. By function extensionality, it suffices to show $\zeta$ and post-composition are equal on $h$ for every $h:{\mathrm{𝗁𝗈𝗆}}_{𝒟}(L(C),Y)$. For each $i:{\mathrm{\Gamma }}_0$, we can build an equality $Q_i:{\psi }^{-1}(\psi (h)\circ r_i)=h\circ L(r_i)$ from ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}$ and the equivalence data for $\psi$. By the SIP for $\mathrm{𝗅𝗂𝗆}$ (Lemma 9), it suffices to prove the following equality for all $i,j:{\mathrm{\Gamma }}_0$ and $g:{\mathrm{\Gamma }}_1(i,j)$:

The problem is that this equality need not hold for wild categories, and we offer an example of an adjunction for which it’s provably false inside HoTT (Example 14). Still, by reverse engineering the equality, we arrive at the following general property of an adjunction as a sufficient condition for it to hold.

Intuitively, Definition 11 accounts for the $2$-dimensional datum introduced by $L(K_{i,j,g})$. This is necessary as the definition of adjunction only accounts for $0$- and $1$-dimensional data. By accounting for the relevant $2$-dimensional data, we can finish porting the standard proof to wild category theory as follows.

This section (along with Section 7) offers evidence that Definition 11 is useful in practice. We show that the suspension endofunctor $\mathrm{\Sigma }:{𝒰}_{\ast }\to {𝒰}_{\ast }$ on the wild category of pointed types is a $2$-coherent left adjoint to the loop space endofunctor $\mathrm{\Omega }$ (which maps $(X,x_0)$ to $\left(x_0=x_0,{\mathrm{𝗋𝖾𝖿𝗅}}_{x_0}\right)$). By Theorem 13, we deduce that $\mathrm{\Sigma }$ preserves (graph-indexed) colimits. Although the diagram ($2$-coh) is a valuable approach to proving this preservation property, it does rely on a new trick based on homogeneous types to handle the path algebra generated by $\mathrm{\Sigma }$. The adjunction $\mathrm{\Sigma }⊣\mathrm{\Omega }$ is already known [8, Lemma 2.16], so our contribution is verifying that $\mathrm{\Sigma }$ is $2$-coherent. Also, to our knowledge, ours is the first proof in HoTT (in particular, Book HoTT) that $\mathrm{\Sigma }$ preserves colimits.

If $X$ is a pointed type, then $\mathrm{𝗍𝗒}(X)$ and $\mathrm{𝗉𝗍}(X)$ denote the underlying type and basepoint of $X$, respectively. If $f:X{\to }_{\ast }Y$ is a pointed map, then $\mathrm{𝖿𝗎𝗇}(f)$ and $\mathrm{𝖻𝗉}(f)$ denote the underlying function and proof of basepoint preservation of $f$, respectively.

The SIP for pointed maps says that the canonical function $f_1=f_2\to f_1{\sim }_{\ast }{f}_2$ is an equivalence, with inverse denoted by $⟨-,-⟩$. We use this equivalence to define the terms ${\mathrm{\Sigma }}_{\circ }$ and ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}$, which will help us manipulate them in the proof of $2$-coherence.

The composition law’s first component is defined by induction (see Section 3.2), with $t_{𝖭}$ and $t_{𝖲}$ trivial and $T$ defined, for suitable pointed maps $r$ and $s$, via the commuting square

Its second component is trivial. The adjunction $\mathrm{\Sigma }⊣\mathrm{\Omega }$ [11, SuspAdjointLoop] is defined by

where the underbrace denotes term abbreviation and $\zeta (\mathrm{𝗀𝗅𝗎𝖾}(x_0),h_0)$ denotes the evident path of type $\xi (x_0,h,h_0)={\mathrm{𝗋𝖾𝖿𝗅}}_{y_0}$. For all $f^{\ast }≔(f,f_0):(Z,z_0){\to }_{\ast }(X,x_0)$ and $h^{\ast }≔(h,h_0):\mathrm{\Sigma }(X,x_0){\to }_{\ast }(Y,y_0)$, ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}(f^{\ast },h^{\ast })$ is defined as the path

Here, for each $z:Z$, $\mathrm{\Theta }(z)$ is defined as the path

and ${\mathrm{\Theta }}_0$ is defined by path induction on ${\rho }_{\mathrm{\Sigma }(f^{\ast })}(z_0)$.

Now that we’ve defined ${\mathrm{\Sigma }}_{\circ }$ and ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}$, we claim that the diagram ($2$-coh) commutes. The SIP for pointed homotopies turns this goal into a double pointed homotopy:

To construct the first component of the desired double pointed homotopy, we have to reduce a large expression involving various $\rho$ terms (coming from the ${\mathrm{𝗇𝖺𝗍}}_{\text{dom}}$ and ${\mathrm{\Sigma }}_{\circ }$ edges of ($2$-coh)). We do so via a mechanical, though nontrivial, process of iteratively eliminating matching $\rho$ terms. The commuting triangle, however, is infeasible to construct directly. The problem is that it contains the entire first component, which involves complex path algebra and does not reduce at $\mathrm{𝗉𝗍}(W)$. In addition, it contains a handful of nontrivial path inductions from $\mathrm{\Theta }$’s second component. The result is an expression that is simply too big.

Luckily, we can get the commuting triangle for free by noticing the special nature of loop spaces. Every loop space is a homogeneous type, i.e., a pointed type $(X,x_0)$ equipped with a pointed equivalence ${\mathrm{𝖺𝗎𝗍𝗈}}_x:(X,x_0){\stackrel{\simeq }{\to }}_{\ast }(X,x)$ for every $x:X$. In this case, we also say $X$ is homogeneous at $x_0$. We note a few things about such types. First, if $M$ is homogeneous, then it’s homogeneous at all its elements. Second, by applying $-\circ {\mathrm{𝖺𝗎𝗍𝗈}}_{\mathrm{𝗉𝗍}(M)}^{-1}$ to $\mathrm{𝖺𝗎𝗍𝗈}$, we can make every homogeneous type $M$ strongly homogeneous, i.e., ${\mathrm{𝖺𝗎𝗍𝗈}}_{\mathrm{𝗉𝗍}(M)}={\mathrm{𝗂𝖽}}_M$. Finally, as $\mathrm{\Omega }$ preserves pointed equivalences, if $(X,x_0)$ is homogeneous, we have $\text{homog-pth}(x_0,x):\left(x_0=x_0\right)\stackrel{\simeq }{\to }\left(x=x\right)$ for every $x:X$. Now, a key insight for our goal is Cavallo’s trick: two pointed maps into homogoneous types are pointed-homotopic when their underlying functions are homotopic [25, $\to \cdot \mathrm{𝙷𝚘𝚖𝚘𝚐𝚎𝚗𝚎𝚘𝚞𝚜}\equiv$]. As our goal is a higher pointed homotopy, we want the following higher version of the trick, which will finish the proof that $\mathrm{\Sigma }$ is $2$-coherent [11, Susp-2coher]:

We end with another application of Theorem 13 in synthetic homotopy theory. We prove that all modalities on coslices of a universe $𝒰$ are $2$-coherent and thereby construct (graph-indexed) colimits of modal types. Consider functions $\mathrm{○}:𝒰\to 𝒰$ and $\eta :{\prod }_{X:𝒰}X\to \mathrm{○}X$. A type $X:𝒰$ is modal if ${\eta }_X$ is an equivalence. Let ${𝒰}_{\mathrm{○}}$ denote the subuniverse of modal types.

Let $\mathrm{○}$ be a modality and $A$ be a type. By $\mathrm{○}$-induction (including the associated nondependent recursion principle), we have a functor ${\mathrm{○}}^A:A/𝒰\to {\left(A/𝒰\right)}_{\mathrm{○}}$ into the full wild subcategory of $A/𝒰$ on those $(X,s)$ with $X$ modal, called modal $A$-types. It is a straightforward extension of the functor $\mathrm{○}:𝒰\to {𝒰}_{\mathrm{○}}$: for example, its object function sends $(X,s)$ to $(\mathrm{○}X,{\eta }_X\circ s)$. By $\mathrm{○}$-induction, we also have a family of equivalences $\left({\mathrm{○}}^{A}U{\to }_{A}V\right)\stackrel{\simeq }{\to }\left(U{\to }_{A}V\right)$ for $A$-types $U$ and modal $A$-types $V$ that is natural in $U$. (It’s trivially natural in $V$.) Hence we have an adjunction between ${\mathrm{○}}^A$ and the forgetful functor ${ℱ}_{\mathrm{○},A}$ [11, Mod-cos-adj].