Document Open Access Logo

On Left Adjoints Preserving Colimits in HoTT

Author Perry Hart

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.20.pdf
  • Filesize: 1.81 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • wild categories
  • colimits
  • adjunctions
  • homotopy type theory
  • category theory
  • synthetic homotopy theory
  • higher inductive types
  • modalities

Metrics

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 prove that the proof may fail for adjunctions between wild categories. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, called 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 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.

Cite As Get BibTex

Perry Hart. On Left Adjoints Preserving Colimits in HoTT. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.20

Author Details

Perry Hart
  • Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN, USA

Funding

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force.

Acknowledgements

The author thanks his PhD advisor, Favonia, for help with writing the extended abstract on the same topic for the HoTT/UF Workshop 2025.

Supplementary Materials

References

  1. Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine. Homotopy limits in type theory. Mathematical Structures in Computer Science, 25(5):1040-1070, 2015. URL: https://doi.org/10.1017/S0960129514000498.
  2. Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types. Journal of Pure and Applied Algebra, 229(6):107963, 2025. URL: https://doi.org/10.1016/j.jpaa.2025.107963.
  3. Ulrik Buchholtz, Tom de Jong, and Egbert Rijke. Epimorphisms and Acyclic Types in Univalent Foundations. The Journal of Symbolic Logic, pages 1-36, 2025. URL: https://doi.org/10.1017/jsl.2024.76.
  4. Paolo Capriotti and Nicolai Kraus. Univalent higher categories via complete Semi-Segal types. Proc. ACM Program. Lang., 2(POPL), 2017. URL: https://doi.org/10.1145/3158132.
  5. Joshua Chen. 2-Coherent Internal Models of Homotopical Type Theory, 2025. URL: https://doi.org/10.48550/arXiv.2503.05790.
  6. Felix Cherubini and Egbert Rijke. Modal descent. Mathematical Structures in Computer Science, 31(4):363-391, 2021. URL: https://doi.org/10.1017/S0960129520000201.
  7. J. Daniel Christensen and Egbert Rijke. Characterizations of modalities and lex modalities. Journal of Pure and Applied Algebra, 226(3):106848, 2022. URL: https://doi.org/10.1016/j.jpaa.2021.106848.
  8. J Daniel Christensen and Luis Scoccola. The Hurewicz theorem in homotopy type theory. Algebraic and Geometric Topology, 23(5):2107-2140, 2023. URL: https://doi.org/10.2140/agt.2023.23.2107.
  9. Thomas M. Fiore. Pseudo Limits, Biadjoints, and Pseudo Algebras: Categorical Foundations of Conformal Field Theory, 2006. URL: https://arxiv.org/abs/math/0408298.
  10. Robert Graham. Synthetic Homology in Homotopy Type Theory, 2018. URL: https://arxiv.org/abs/1706.01540.
  11. Perry Hart. PHart3/colimits-agda, 2025. Software (visited on 2026-01-23). URL: https://github.com/PHart3/colimits-agda/tree/lapc
    full metadata available at: https://doi.org/10.4230/artifacts.25210
  12. Perry Hart and Kuen-Bang Hou (Favonia). Coslice Colimits in Homotopy Type Theory. In Jörg Endrullis and Sylvain Schmitz, editors, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), volume 326 of Leibniz International Proceedings in Informatics (LIPIcs), pages 46:1-46:20, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2025.46.
  13. Nicolai Kraus. Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT, 2021. URL: https://arxiv.org/abs/2009.01883.
  14. Nicolai Kraus and Jakob von Raumer. Path Spaces of Higher Inductive Types in Homotopy Type Theory . In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, Los Alamitos, CA, USA, June 2019. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2019.8785661.
  15. Daniel R. Licata and Guillaume Brunerie. A Cubical Approach to Synthetic Homotopy Theory. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 92-103, 2015. URL: https://doi.org/10.1109/LICS.2015.19.
  16. Daniel R. Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603153.
  17. Axel Ljungström. Symmetric monoidal smash products in homotopy type theory. Mathematical Structures in Computer Science, 34(9):985-1007, 2024. URL: https://doi.org/10.1017/S0960129524000318.
  18. Peter Lefanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020. URL: https://doi.org/10.1017/S030500411900015X.
  19. Saunders MacLane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer, 1978. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  20. Anders Mörtberg and Loïc Pujet. Cubical synthetic homotopy theory. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 158-171, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373825.
  21. Emily Riehl. Category Theory in Context. Aurora: Dover Modern Math Originals. Dover Publications, 2016. Google Scholar
  22. Egbert Rijke. Introduction to Homotopy Type Theory, 2022. URL: https://arxiv.org/abs/2212.11082.
  23. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  24. Michael Shulman. All (∞,1)-toposes have strict univalent universes, 2019. URL: https://arxiv.org/abs/1904.07004.
  25. The Agda Community. Cubical Agda Library, February 2025. version 0.8. URL: https://github.com/agda/cubical.
  26. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  27. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming, 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact