Document Open Access Logo

Choice Principles and Hypercompletion in HoTT

Author Owen Milner

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.1.pdf
  • Filesize: 0.63 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • HoTT
  • hypercompletion
  • modalities

Metrics

Abstract

Building on work of Anel and Barton [M. Anel and R. Barton, 2024], we will introduce the construction of a hypercompletion modality [E. Rijke et al., 2020] in HoTT under the assumption that countable choice holds. Central results have been formalized in Cubical Agda and will be referenced where appropriate.

Cite As Get BibTex

Owen Milner. Choice Principles and Hypercompletion in HoTT. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.1

Author Details

Owen Milner
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009, PI Steve Awodey.

Acknowledgements

I want to thank Mathieu Anel, Steve Awodey, Reid Barton, and Hugo Moeneclaey for helpful discussions.

References

  1. M. Anel and R. Barton. Choice axioms and postnikov completeness, 2024. URL: https://arxiv.org/abs/2403.19772.
  2. F. Cherubini, T. Coquand, F. Geerligs, and H. Moeneclaey. A foundation for synthetic stone duality. In R. E. Møgelberg and B. van den Berg, editors, 30th International Conference on Types for Proofs and Programs (TYPES 2024), 2025. Google Scholar
  3. L. Leclerc. Cohomology in homotopy type theory. Internship Report, 2022. Google Scholar
  4. J. Lurie. Higher Topos Theory. Princeton University Press, 2009. Google Scholar
  5. O. Milner. Github Repository. URL: https://github.com/owen-milner/choicepostnikov.
  6. M. M. Postnikov. Investigations in the homotopy theory of continuous mappings. American Mathematical Society Translations, 7, 1957. Google Scholar
  7. E. Rijke. Introduction to Homotopy Type Theory. Cambridge University Press, 2026. Google Scholar
  8. E. Rijke, M. Shulman, and B. Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  9. The Univalent Foundations Program. Homotopy type theory: Univalent foundations for mathematics, 2013. URL: https://homotopytypetheory.org/book/.
  10. F. van Doorn. On the formalization of higher inductive types and synthetic homotopy theory. PhD thesis, Carnegie Mellon University, 2018. Google Scholar
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact