{"id":"arxiv/2608.28473","url":"https://arxiv.org/abs/2608.28473","tags":["cs.LO","math.CT"],"score":0,"title":"On Left Adjoints Preserving Colimits in Homotopy Type Theory","domain":"cs.LO","source":"arxiv","authors":["Perry Hart"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-28","reactions":{}}