On Left Adjoints Preserving Colimits in Homotopy Type Theory
Abstract
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.
Related
- Stable homotopy theory of higher categories with adjoints
- Parabolic Homotopy Colimits and Coxeter Descents
- A support preserving homotopy for the de Rham complex with boundary decay estimates
- On the internal homotopy theory of motivic categories
- Compact quotients of homogeneous spaces and homotopy theory of sphere bundles
BibTeX
@misc{hart2026left,
title = {{On Left Adjoints Preserving Colimits in Homotopy Type Theory}},
author = {Perry Hart},
howpublished = {arXiv},
year = {2026},
month = aug,
doi = {10.48550/arxiv.2608.28473},
eprint = {2608.28473},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.28473},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - On Left Adjoints Preserving Colimits in Homotopy Type Theory
AU - Perry Hart
PY - 2026
DA - 2026/08/28
PB - arXiv
DO - 10.48550/arxiv.2608.28473
UR - https://arxiv.org/abs/2608.28473
AB - 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.
ER -