Coslice Colimits in Homotopy Type Theory

Authors Perry Hart , Kuen-Bang Hou (Favonia)



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.46.pdf
  • Filesize: 0.91 MB
  • 20 pages

Document Identifiers

Author Details

Perry Hart
  • Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN, USA
Kuen-Bang Hou (Favonia)
  • Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN, USA

Acknowledgements

We thank the anonymous reviewers for their feedback that improved the writing of this paper. We also thank the anonymous reviewer for HoTT/UF 2023 who pointed out the relationship between adjunctions and factorization systems.

Cite As Get BibTex

Perry Hart and Kuen-Bang Hou (Favonia). Coslice Colimits in Homotopy Type Theory. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 46:1-46:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.46

Abstract

We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between colimits in coslices of a universe, called coslice colimits, and colimits in the universe (i.e., ordinary colimits). To derive this characterization, we find an explicit construction of colimits in coslices that is tailored to reveal the connection. We use the construction to derive properties of colimits. Notably, we prove that the forgetful functor from a coslice creates colimits over trees. We also use the construction to examine how colimits interact with orthogonal factorization systems and with cohomology theories. As a consequence of their interaction with orthogonal factorization systems, all pointed colimits (special kinds of coslice colimits) preserve n-connectedness, which implies that higher groups are closed under colimits on directed graphs. We have formalized our main construction of the coslice colimit functor in Agda.

Subject Classification

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

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Ulrik Buchholtz and Kuen-Bang Hou (Favonia). Cellular Cohomology in Homotopy Type Theory. Logical Methods in Computer Science, Volume 16, Issue 2, 2020. URL: https://doi.org/10.23638/LMCS-16(2:7)2020.
  2. Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke. Higher Groups in Homotopy Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 205-214, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209150.
  3. 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.
  4. Evan Cavallo. Synthetic Cohomology in Homotopy Type Theory. Master’s thesis, Carnegie Mellon University, 2015. URL: https://staff.math.su.se/evan.cavallo/works/thesis15.pdf.
  5. 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.
  6. Perry Hart and Kuen-Bang Hou. Coslice Colimits in Homotopy Type Theory, 2024. URL: https://arxiv.org/abs/2411.15103.
  7. Perry Hart and Kuen-Bang Hou (Favonia). A formalized construction of coslice colimits, 2024. v0.1.0. URL: https://github.com/PHart3/colimits-agda/tree/v0.1.0.
  8. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 565-574, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934545.
  9. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). J. Eur. Math. Soc., 23(6):2071-2126, 2021. URL: https://doi.org/10.4171/JEMS/1050.
  10. Max Kelly. On MacLane’s Conditions for Coherence of Natural Associativities, Commutativities, etc. Journal of Algebra, 1(4):397-402, 1964. URL: https://doi.org/10.1016/0021-8693(64)90018-3.
  11. 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.
  12. 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.
  13. 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.
  14. Jacob Lurie. Higher Algebra. Unpublished, 2017. URL: https://www.math.ias.edu/~lurie/papers/HA.pdf.
  15. Jacob Lurie. Kerodon. https://kerodon.net, 2024.
  16. nLab authors. created limit. https://ncatlab.org/nlab/show/created+limit, 2024. URL: https://ncatlab.org/nlab/revision/created+limit/21.
  17. nLab authors. (infinity,1)-limit. https://ncatlab.org/nlab/show/%28%E2%88%9E%2C1%29-limit, 2024. URL: https://ncatlab.org/nlab/revision/%28%E2%88%9E%2C1%29-limit/78.
  18. nLab authors. pointed abelian group. https://ncatlab.org/nlab/show/pointed+abelian+group, November 2024. URL: https://ncatlab.org/nlab/revision/pointed+abelian+group/3.
  19. nLab authors. pullback-stable colimit. https://ncatlab.org/nlab/show/pullback-stable+colimit, October 2024. URL: https://ncatlab.org/nlab/revision/pullback-stable+colimit/18.
  20. Emily Riehl. Categorical Homotopy Theory. New Mathematical Monographs. Cambridge University Press, 2014. URL: https://doi.org/10.1017/CBO9781107261457.
  21. Egbert Rijke. Introduction to Homotopy Type Theory, 2022. URL: https://arxiv.org/abs/2212.11082.
  22. 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.
  23. Egbert Rijke, Elisabeth Stenholm, Jonathan Prieto-Cubides, Fredrik Bakke, and others. The agda-unimath library. URL: https://github.com/UniMath/agda-unimath/.
  24. Kristina Sojakova. Higher Inductive Types as Homotopy-Initial Algebras. SIGPLAN Not., 50(1):31-42, 2015. URL: https://doi.org/10.1145/2775051.2676983.
  25. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 845-858, 2020. URL: https://doi.org/10.1145/3373718.3394801.
  26. Ross Street. Limits indexed by category-valued 2-functors. Journal of Pure and Applied Algebra, 8(2):149-181, 1976. URL: https://doi.org/10.1016/0022-4049(76)90013-X.
  27. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  28. Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. Homotopy Type Theory in Lean. In Interactive Theorem Proving, pages 479-495. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_30.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail