Source-linked AI summary
On Left Adjoints Preserving Colimits in Homotopy Type Theory
Perry Hart
TL;DR
The paper asks whether the standard proof that left adjoints preserve colimits extends to wild categories, where hidden coherence can make the proof fail and colimit preservation itself fail. It identifies 2-coherence as a sufficient condition, verifies it for suspension and modalities, and derives corresponding colimit results.
Problem
In wild categories, the standard proof may fail because hom-adjunction data uses less structure than the composition law used to construct the induced cocone.
Method
The paper formulates 2-coherence as a sufficient condition ensuring compatibility between hom-isomorphism naturality and the left adjoint’s composition law.
Results
2-coherence makes the induced cocone colimiting; suspension and joins satisfy it for graph-indexed colimits, and modalities on coslices are 2-coherent.
Takeaways & Limitations
The results establish colimit preservation for suspension and modal subcategories while providing a standard-proof criterion applicable to wild adjunctions.
Takeaways & Limitations
The direct construction of a key commuting triangle for suspension is infeasible because it contains a complex first component involving path algebra.
Abstract
from arXiv · showhide
We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We show that the proof may fail for adjunctions between wild categories and even produce a wild left adjoint that fails to preserve colimits. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, which we call 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor, as well as a generalization thereof, preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda.
1. Introduction
In wild categories, the classical theorem that left adjoints preserve colimits can fail because proof-relevant composition data creates coherence problems. The paper introduces 2-coherence and applies it to suspension, joins, and modalities.
- Wild categories omit higher coherence data while retaining enough structure to study colimits and adjunctions in homotopy type theory.
- The standard proof of colimit preservation can fail for wild adjunctions, including an example whose left adjoint does not preserve colimits.
- 2-coherence requires the hom-adjunction naturality structure to agree with the left adjoint’s proof-relevant composition law.
- The paper proves that 2-coherent left adjoints preserve colimits using algebraic manipulation of adjunction data and foundational HoTT principles.
- Suspension and the unary join satisfy 2-coherence, with a higher homogeneous-type trick avoiding an infeasible direct equality proof.
- Every modality on a universe coslice is 2-coherent, yielding colimits for the associated modal subcategories; the main results are formalized in Agda.
2. Additional related work
The paper situates its study within wild-category coherence research and builds its suspension application on homogeneous types and Cavallo’s trick.
- The work extends research on wild categories by adding higher coherence conditions that internalize aspects of higher categorical structure.
- The suspension application uses homogeneous types, whose basepoint independence makes identities about pointed maps easier to prove.
- Its discussion contrasts the paper’s findings with a prior claim that the Book proof matches the usual classical proof.
3. Background on type theory
The background develops path action, equivalences, transport, and pushout-based suspension constructions used later in the wild-categorical arguments.
- The function ap maps paths through functions and provides the functorial action on morphisms of types viewed as ∞-groupoids.
- Homotopy naturality gives a commuting identity square relating path actions of homotopic functions.
- A half-adjoint equivalence consists of an inverse, two homotopies, and a triangle identity, and equivalently can be characterized by bi-invertibility.
- Transport supplies the dependent analogue of ap and is essential for induction principles of higher inductive types.
- Suspension is defined as the cofiber of X → 1, hence as a pushout with two distinguished points and glue paths.
- Pointed suspension maps are defined by recursion and satisfy a computation rule mapping each glue path to the corresponding glue path.
4. Wild category theory
Wild category theory supplies type-valued morphisms, proof-relevant composition, hom-type adjunctions, and graph-indexed cocones needed for the paper’s preservation theorem.
- Wild categories differ from internalized 1-categories because their hom types may have nontrivial identity types and omit higher coherence data.
- A wild category has objects, hom types, identities, composition, unit laws, and associativity paths rather than judgmentally strict equations.
- Wild functors include object and morphism actions together with proof-relevant composition and identity data.
- A wild adjunction is a family of hom-type equivalences equipped with naturality witnesses in both variables.
- The paper’s adjunction results do not use functor identity data or one naturality component, showing these fields could be omitted for its purposes.
- Because general coherence towers remain unresolved in HoTT, the development restricts diagrams to graphs and represents cocones through limits of hom types.
- Limits are functorial, preserve equivalences induced by natural isomorphisms, and admit a structure identity principle used to port the LAPC proof.
5. Porting the proof of LAPC
The standard proof that left adjoints preserve colimits can fail for wild categories because its required equality need not hold. The paper introduces 2-coherence as a sufficient condition, proves colimit preservation under it, and gives examples showing both proof failure and an actual preservation failure.
- 2-coherence: 2-coherence requires the adjunction’s naturality structure to interact coherently with the left adjoint’s proof-relevant composition law.The condition is formalized as commutativity for suitable morphisms and accounts for the relevant 2-dimensional datum.
- Failure of the standard proof: Without 2-coherence, the standard proof can fail because a required equality is not generally forced in wild categories.The equality would be automatic when hom types are sets, but Example 5.5 gives a wild adjunction where it is provably false.
- The sufficient condition: If L is 2-coherent, the induced cocone L(K) is colimiting whenever K is colimiting.The proof compares the hom-isomorphism-induced map with post-composition, using naturality, equivalence identities, and the structure identity principle.
- Failure versus preservation: Example 5.5 shows that proof failure does not imply colimit failure: its wild adjunction Λ preserves graph-indexed colimits despite lacking 2-coherence.Thus 2-coherence is sufficient but not necessary for preservation of colimits.
- An actual counterexample: Example 5.6 constructs a wild adjunction whose left adjoint sends a colimiting cocone to a non-colimiting cocone.The original cocone K is colimiting, whereas Λ(K) is not because the relevant post-composition map has an empty fiber over (base, loop).
- Scope of the counterexamples: The counterexamples persist even when the wild categories are bicategories, so adding bicategorical structure does not resolve the cocontinuity problem.The issue is distinct from the failure of triangle and pentagon identities in another wild category construction.
6. Suspension is 2-coherent
The suspension functor is shown to be 2-coherent, allowing the standard left-adjoint preservation proof to establish graph-indexed colimit preservation. A higher Cavallo-style trick for homogeneous types avoids an infeasible direct equality proof and yields consequences for acyclic types and generalized joins.
- 2-coherence and preservation: The suspension endofunctor Σ is 2-coherent as a left adjoint to loop space Ω, so it preserves graph-indexed colimits.The adjunction was already known; the contribution is verifying 2-coherence.
- Proof strategy: The direct construction is infeasible because the required expression contains complex path algebra, nontrivial path inductions, and becomes too large.The large expression arises from β-rules associated with naturality and composition data.
- 2-coherence and preservation: A higher version of Cavallo’s trick reduces the difficult commuting-triangle proof by exploiting that loop spaces are homogeneous types.Homogeneous types make identities about pointed maps easier to prove, while strong homogeneity supplies the needed triangle.
- Consequences: Pointed acyclic types are closed under colimits in U∗.This follows by transporting colimits through suspension and using that the resulting cofiber is contractible.
- Generalization: The join functor X ∗− generalizes suspension and has a corresponding adjunction, reducing to the suspension-loop adjunction when X is the pointed type 2.The same 2-coherence argument applies to this generalization.
7. Colimits of modal types
For a modality on a universe, the induced functor on coslices is a 2-coherent left adjoint to the forgetful functor. Consequently, the wild category of modal types in each coslice has all graph-indexed colimits.
- Modal coslice adjunction: The induced functor #A sends A-types to modal A-types and has an adjunction with the forgetful functor.Its object function maps (X,s) to (#X, ηX ◦s), and modality induction supplies the required natural equivalences.
- 2-coherence: The left adjoint #A is 2-coherent.The proof is described as #-induction followed by path induction.
- Colimits of modal types: The wild category (A/U)# of modal A-types has all colimits.The construction uses colimits in A/U and the fact that #A preserves them.
- Comparison with the Book proof: The colimit construction is simpler than the Book proof and makes explicit a higher coherence between a modality’s composition law and naturality data.For truncation, the relevant coherence follows from the definitional equality ∥g ◦f∥n ◦|−|n ≡|−|n ◦g ◦f.
8. Conclusion and future work
The paper identifies 2-coherence as the sufficient condition restoring the left-adjoint colimit argument for wild categories, verifies it for suspension, joins, and modal coslices, and derives cocompleteness results. It leaves duality, reflective subuniverses, and smash-product coherence as open directions.
- Conclusion: In wild categories, the classical coherence needed for left adjoints to preserve colimits can fail, and a wild left adjoint may fail to preserve colimits outright.The paper provides an example inside HoTT exhibiting both the proof failure and the stronger preservation failure.
- Conclusion: 2-coherence is identified as a tractable sufficient condition making the standard preservation proof work.The paper verifies this condition for suspension and uses a higher homogeneous-type trick to complete the proof.
- Conclusion: Modalities on coslices of a universe are shown to be 2-coherent, making the associated subcategories of modal types cocomplete.This is the paper’s second principal application of the coherence condition.
- Future work: Open questions concern the dual right-adjoint statement, extending the modality result to all reflective subuniverses, and proving smash-product 2-coherence in Book HoTT.The smash-product case lacks the homogeneous-type target needed for the existing escape from the infeasible equality proof.