AI 中文总结
该研究在同伦类型论的野生范畴环境中，提出左伴随保持余极限的2-协调性充分条件，证明悬置函子等保持余极限，并形式化结果于Agda。
AI 中文摘要
我们研究了“左伴随保持余极限”这一标准证明在野生范畴中的表现，野生范畴是同伦类型论内部合成同伦理论的自然环境。我们证明该证明对于野生范畴之间的伴随可能失效，甚至会产生不保持余极限的野生左伴随。然而，我们的核心贡献是给出了左伴随满足证明成立的充分条件，该条件被称为2-协调性，它表示同构的自然性结构与态射的复合可交换。我们给出了该条件应用的两个实用示例：首先，结合同伦类型论中齐次类型已知技巧的新版本，证明了悬置函子及其推广形式保持图索引的余极限；其次，将每个模态视为类型宇宙余切片上的函子，证明其作为模态类型子范畴忘却函子的左伴随是2-协调的，从而证明该子范畴是余完备的。我们已在Agda中形式化了主要结果。
英文摘要
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.
CommentsAgda code: https://github.com/PHart3/colimits-agda/tree/lapc-lmcs
