Document Open Access Logo

The Rezk Completion for Elementary Topoi

Authors Kobe Wullaert , Niels van der Weide

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.8.pdf
  • Filesize: 0.86 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • univalent foundations
  • univalent categories
  • Rezk completions
  • UniMath
  • formalization
  • elementary topoi

Metrics

Abstract

The development of category theory in univalent foundations and the formalization thereof is an active field of research. Categories in that setting are often assumed to be univalent which means that identities and isomorphisms of objects coincide. One consequence hereof is that equivalences and identities coincide for univalent categories and that structure on univalent categories transfers along equivalences. However, constructions such as the Kleisli category, the Karoubi envelope, and the tripos-to-topos construction, do not necessarily give univalent categories. To deal with that problem, one uses the Rezk completion, which completes a category into a univalent one. However, to use the Rezk completion when considering categories with structure, one also needs to show that the Rezk completion inherits the structure from the original category.
In this work, we present a modular framework for lifting the Rezk completion from categories to categories with structure. We demonstrate the modularity of our framework by lifting the Rezk completion from categories to elementary topoi in manageable steps.

Cite As Get BibTex

Kobe Wullaert and Niels van der Weide. The Rezk Completion for Elementary Topoi. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 8:1-8:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.8

Author Details

Kobe Wullaert
  • Delft University of Technology, The Netherlands
Niels van der Weide
  • Radboud University, Nijmegen, The Netherlands

Funding

  • van der Weide, Niels: This research was supported by the NWO project "The Power of Equality" OCENW.M20.380, which is financed by the Dutch Research Council (NWO).

Acknowledgements

We thank Benedikt Ahrens for valuable feedback on the versions of this paper and for the many helpful discussions. Furthermore, we thank Arnoud van der Leer for reviewing the formalization and for refactoring the material on cartesian closed categories. We gratefully acknowledge the work by the Rocq development team in providing the Rocq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Rocq.

Supplementary Materials

References

  1. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in univalent foundations. Math. Struct. Comput. Sci., 31(10):1232-1269, 2021. URL: https://doi.org/10.1017/S0960129522000032.
  2. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Math. Struct. Comput. Sci., 25(5):1010-1039, 2015. URL: https://doi.org/10.1017/S0960129514000486.
  3. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, Volume 15, Issue 1, March 2019. URL: https://doi.org/10.23638/LMCS-15(1:20)2019.
  4. Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:18)2018.
  5. Benedikt Ahrens, Paige North, Michael Shulman, and Dimitris Tsementzis. The Univalence Principle. Memoirs of the American Mathematical Society, 305(1541):vii+176, 2025. URL: https://doi.org/10.1090/memo/1541.
  6. Francis Borceux. Handbook of Categorical Algebra: Volume 1, Basic category theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994. Google Scholar
  7. 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.
  8. Tom de Jong and Martín Hötzel Escardó. Examples and counterexamples of injective types. arXiv preprint arXiv:2601.12536, 2026. URL: https://doi.org/10.48550/arXiv.2601.12536.
  9. M. P. Fourman and A. Ščedrov. The “world’s simplest axiom of choice” fails. manuscripta mathematica, 38(3):325-332, 1982. URL: https://doi.org/10.1007/BF01170929.
  10. Jonas Frey. Characterizing partitioned assemblies and realizability toposes. Journal of Pure and Applied Algebra, 223(5):2000-2014, 2019. URL: https://doi.org/10.1016/j.jpaa.2018.08.012.
  11. Denis Higgs. Injectivity in the Topos of Complete Heyting Algebra Valued Sets. Canadian Journal of Mathematics, 36(3):550-568, 1984. URL: https://doi.org/10.4153/CJM-1984-034-4.
  12. J. Martin E. Hyland. Classical lambda calculus in modern dress. Mathematical Structures in Computer Science, 27(5):762-781, 2017. URL: https://doi.org/10.1017/S0960129515000377.
  13. John Martin Elliott Hyland, Peter Tennant Johnstone, and Andrew Mawdesley Pitts. Tripos theory. Mathematical Proceedings of the Cambridge Philosophical Society, 88(2):205-232, 1980. URL: https://doi.org/10.1017/S0305004100057534.
  14. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6):2071-2126, 2021. URL: https://doi.org/10.4171/JEMS/1050.
  15. F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43(1):135-166, 1973. URL: https://doi.org/10.1007/BF02924844.
  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. Maria Emilia Maietti. Joyal’s arithmetic universe as list-arithmetic pretopos. Theory and Applications of Categories, 24, January 2010. URL: https://doi.org/10.70930/tac/qee78enb.
  18. Ieke Moerdijk and Erik Palmgren. Wellfounded trees in categories. Annals of Pure and Applied Logic, 104(1):189-218, 2000. URL: https://doi.org/10.1016/S0168-0072(00)00012-9.
  19. Andrew Mawdesley Pitts. Tripos Theory in Retrospect. Math. Struct. Comput. Sci., 12(3):265-279, 2002. URL: https://doi.org/10.1017/S096012950200364X.
  20. Nima Rasekh, Niels van der Weide, Benedikt Ahrens, and Paige Randall North. Insights from Univalent Foundations: A Case Study Using Double Categories. 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 45:1-45:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2025.45.
  21. Ross Street. Two-dimensional sheaf theory. Journal of Pure and Applied Algebra, 23(3):251-270, 1982. URL: https://doi.org/10.1016/0022-4049(82)90101-3.
  22. The Rocq Development Team. The Rocq Prover, April 2025. URL: https://doi.org/10.5281/zenodo.15149629.
  23. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  24. Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens. Scott’s Representation Theorem and the Univalent Karoubi Envelope. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025, volume 352 of LIPIcs, pages 33:1-33:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.33.
  25. Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 4:1-4:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.4.
  26. Niels van der Weide. The Formal Theory of Monads, Univalently. Logical Methods in Computer Science, Volume 21, Issue 1, February 2025. URL: https://doi.org/10.46298/lmcs-21(1:16)2025.
  27. Niels van der Weide. The internal languages of univalent categories. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 112-126, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00016.
  28. Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North. Univalent Double Categories. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pages 246-259, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3636501.3636955.
  29. Jaap van Oosten. Realizability: An Introduction to Its Categorical Side, volume 152 of Studies in Logic and the Foundations of Mathematics. Elsevier B. V., Amsterdam, 2008. Google Scholar
  30. Niccolò Veltri and Niels van der Weide. Constructing Higher Inductive Types as Groupoid Quotients. Logical Methods in Computer Science, Volume 17, Issue 2, April 2021. URL: https://doi.org/10.23638/LMCS-17(2:8)2021.
  31. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at http://unimath.github.io/UniMath/, 2024. URL: https://doi.org/10.5281/zenodo.13828995.
  32. Mark Weber. Yoneda Structures from 2-toposes. Applied Categorical Structures, 15(3):259-323, 2007. URL: https://doi.org/10.1007/s10485-007-9079-2.
  33. Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, volume 269 of LIPIcs, pages 15:1-15:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.TYPES.2022.15.
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