Document Open Access Logo

Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations

Authors Evan Cavallo , Thierry Coquand

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.10.pdf
  • Filesize: 1.03 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Homotopy type theory
  • axiom of replacement
  • univalent completion
  • higher inductive type
  • cubical sets

Metrics

Abstract

We study Rijke’s type theoretic axiom of replacement, which closes a type-theoretic universe under certain images, and its cousin the axiom of univalent completions, which postulates an extension of each type family to a univalent family. In a long expository section, we survey applications of these two axioms in the literature, from the construction of truncations to the construction of Eilenberg-MacLane spaces to the interpretation of material set theory, making a case for their value as foundational principles. We then give direct, constructive interpretations of the axioms in cubical sets models of type theory and suggest how they can be understood as higher inductive constructions.

Cite As Get BibTex

Evan Cavallo and Thierry Coquand. Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.10

Author Details

Evan Cavallo
  • Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden
Thierry Coquand
  • Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Cavallo, Evan: Knut and Alice Wallenberg Foundation (KAW), Grant No. 2019.0116.
  • Coquand, Thierry: ForCUTT project, ERC advanced grant 101053291.

Acknowledgements

We thank David Wärn for introducing us to univalent completion and for supplying the proof of Proposition 17, which relates completion to replacement. We thank Amélia Liao and David Wärn for independently pointing out a simplification of our original inductive recursive formulation of replacement. We thank our reviewers for thorough comments.

References

  1. Peter Aczel. The type theoretic interpretation of constructive set theory. In Logic Colloquium '77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 55-66. Elsevier, 1978. URL: https://doi.org/10.1016/S0049-237X(08)71989-X.
  2. Peter Aczel and Michael Rathjen. CST book draft, 2010. version from August 19, 2010. URL: https://michrathjen.github.io/book.pdf.
  3. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. In Maria del Mar González, Paul C. Yang, Nicola Gambino, and Joachim Kock, editors, Extended Abstracts Fall 2013, pages 75-76. Springer International Publishing, 2015. URL: https://doi.org/10.1007/978-3-319-21284-5_14.
  4. Álvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren. A univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science, 25(5):1147-1171, 2015. URL: https://doi.org/10.1017/S0960129514000541.
  5. Mathieu Anel. The category of π-finite spaces. Journal of Pure and Applied Algebra, 229(6):107925, 2025. URL: https://doi.org/10.1016/j.jpaa.2025.107925.
  6. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of cartesian cubical type theory. Math. Structures in Comput. Sci., 31(4), 2021. URL: https://doi.org/10.1017/S0960129521000347.
  7. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 6:1-6:17, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.6.
  8. Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, editors. Théorie des topos et cohomologie étale des schémas: Séminaire de Géométrie Algébrique du Bois-Marie, 1963/64, SGA 4, Tome 1, volume 269 of Lecture Notes in Mathematics. Springer-Verlag, 1972. URL: https://doi.org/10.1007/BFb0081551.
  9. Henning Basold, Herman Geuvers, and Niels van der Weide. Higher inductive types in programming. Journal of Universal Computer Science, 23(1):63-88, 2017. URL: https://doi.org/10.3217/jucs-023-01-0063.
  10. Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry, 2026. Commit: https://github.com/UniMath/SymmetryBook/tree/ca373545a0054cc1dac6d376fb58285df434ebdb. URL: https://unimath.github.io/SymmetryBook/book.pdf.
  11. Marc Bezem, Ulrik Buchholtz, Daniel R. Grayson, and Michael Shulman. Construction of the circle in UniMath. Journal of Pure and Applied Algebra, 225(10), 2021. URL: https://doi.org/10.1016/j.jpaa.2021.106687.
  12. Rafaël Bocquet. Strict Rezk completions of models of HoTT and homotopy canonicity, 2023. URL: https://doi.org/10.48550/arXiv.2311.05849.
  13. Ulrik Buchholtz. Proof theory of homotopy type theory: what we know so far, 2016. Slides from a talk at FOMUS - Foundations of Mathematics: Univalent foundations and set theory. URL: https://ulrikbuchholtz.dk/bielefeld-proof-theory.pdf.
  14. 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.
  15. 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. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209150.
  16. Timothy Campion. Cubical sites as Eilenberg-Zilber categories, 2023. URL: https://arxiv.org/abs/2303.06206.
  17. Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. Proceedings of the ACM on Programming Languages, 3(POPL):1:1-1:27, 2019. URL: https://doi.org/10.1145/3290314.
  18. Evan Cavallo, Anders Mörtberg, and Andrew W. Swan. Unifying cubical models of univalent type theory. In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152, pages 14:1-14:17, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.14.
  19. Evan Cavallo and Christian Sattler. The algebraic small object argument as a saturation, 2025. URL: https://arxiv.org/abs/2506.02759.
  20. Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A foundation for synthetic algebraic geometry. Mathematical Structures in Computer Science, 34(9):1008-1053, 2024. URL: https://doi.org/10.1017/S0960129524000239.
  21. J. Daniel Christensen. A characterization of univalent fibrations, June 2015. Slides from a talk at Category Theory 2015 (CT2015). URL: https://jdc.math.uwo.ca/papers/univalence-ct2015.pdf.
  22. J. Daniel Christensen. Non-accessible localizations. Journal of Topology, 17(2):e12336, 2024. URL: https://doi.org/10.1112/topo.12336.
  23. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs, TYPES 2015, pages 5:1-5:34, 2015. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  24. Thierry Coquand and Jonas Höfer. Poset type theory, 2024. Presented at the 30th International Conference on Types for Proofs and Programs, TYPES 2024. URL: https://vipwww.itu.dk/research/types2024/abstracts.pdf.
  25. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  26. Tom de Jong. Domain Theory in Constructive and Predicative Univalent Foundations. PhD thesis, University of Birmingham, 2023. URL: https://doi.org/10.48550/arXiv.2301.12405.
  27. Tom de Jong and Martín Hötzel Escardó. On small types in univalent foundations. Logical Methods in Computer Science, 19(2):8:1-8:33, 2023. URL: https://doi.org/10.46298/LMCS-19(2:8)2023.
  28. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525-549, 2000. URL: https://doi.org/10.2307/2586554.
  29. Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124(1):1-47, 2003. URL: https://doi.org/10.1016/S0168-0072(02)00096-9.
  30. Samuel Eilenberg and Saunders MacLane. Relations between homology and homotopy groups of spaces. ii. Annals of Mathematics, 51(3):514-533, 1950. URL: https://doi.org/10.2307/1969365.
  31. José Ferreirós. Labyrinth of Thought: A History of Set Theory and Its Role in Modern Mathematics. Birkhäuser Basel, 2007. Google Scholar
  32. Abraham A. Fraenkel. Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre. Mathematische Annalen, 86:230-237, 1922. URL: https://doi.org/10.1007/BF01457986.
  33. David Gepner and Joachim Kock. Univalence in locally cartesian closed ∞-categories. Forum Mathematicum, 29(3):617-652, 2017. URL: https://doi.org/10.1515/forum-2015-0228.
  34. Håkon Robbestad Gylterud. From multisets to sets in homotopy type theory. Journal of Symbolic Logic, 83(3):1132-1146, 2018. URL: https://doi.org/10.1017/jsl.2017.84.
  35. Håkon Robbestad Gylterud and Elisabeth Stenholm. Univalent material set theory, 2024. URL: https://arxiv.org/abs/2312.13024.
  36. Michael Hallett. Cantorian set theory and limitation of size. Number 10 in Oxford Logic Guides. Clarendon Press, 1984. Google Scholar
  37. Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, and Thorsten Altenkirch. Small induction recursion. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications, pages 156-172, 2013. URL: https://doi.org/10.1007/978-3-642-38946-7_13.
  38. Akihiro Kanamori. In praise of replacement. Bulletin of Symbolic Logic, 18(1):46-90, 2012. URL: https://doi.org/10.2178/bsl/1327328439.
  39. Ambrus Kaposi and András Kovács. Signatures and induction principles for higher inductive-inductive types. Logical Methods in Computer Science, 16(1), 2020. URL: https://doi.org/10.23638/lmcs-16(1:10)2020.
  40. 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.
  41. Azriel Lévy. Axiom schemata of strong infinity in axiomatic set theory. Pacific Journal of Mathematics, 10(1):223-238, 1960. Google Scholar
  42. Daniel R. Licata and Eric Finster. Eilenberg-maclane spaces in homotopy type theory. In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-9. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603153.
  43. Per Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  44. Per Martin-Löf. Constructive Mathematics and Computer Programming, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153-175. Elsevier, 1982. URL: https://doi.org/10.1016/s0049-237x(09)70189-2.
  45. Richard Montague. Fraenkel’s addition to the axioms of Zermelo. In Yehoshua Bar-Hillel, E. I. J. Poznanski, M. O. Rabin, and Abraham Robinson, editors, Essays on the foundations of mathematics, pages 91-114. Magnes Press, 1961. Google Scholar
  46. John Myhill. Constructive set theory. Journal of Symbolic Logic, 40(3):347-382, 1975. URL: https://doi.org/10.2307/2272159.
  47. Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  48. Nima Rasekh. Univalence in higher category theory, 2021. URL: https://arxiv.org/abs/2103.12762.
  49. Michael Rathjen. Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory. Annals of Pure and Applied Logic, 136:156-174, 2005. URL: https://doi.org/10.1016/j.apal.2005.05.010.
  50. Michael Rathjen. Proof Theory of Constructive Systems: Inductive Types and Univalence, volume 13 of Outstanding Contributions to Logic, pages 385-419. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-63334-3_14.
  51. Egbert Rijke. The join construction, 2017. URL: https://arxiv.org/abs/1701.07538.
  52. Egbert Rijke. Topics in synthetic homotopy theory. PhD thesis, Carnegie Mellon University, 2018. URL: https://arxiv.org/abs/1906.09435.
  53. Egbert Rijke. Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2025. URL: https://doi.org/10.1017/9781108933568.
  54. Egbert Rijke and Bas Spitters. Sets in homotopy type theory. Mathematical Structures in Computer Science, 25(5):1172-1202, 2015. URL: https://doi.org/10.1017/S0960129514000553.
  55. Christian Sattler and Andrea Vezzosi. Partial univalence in n-truncated type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '20), pages 807-819, 2020. URL: https://doi.org/10.1145/3373718.3394759.
  56. Michael Shulman. Higher inductive-recursive univalence and type-directed definitions, 2014. Blog post on the Homotopy Type Theory blog. URL: https://homotopytypetheory.org/2014/06/08/hiru-tdd/.
  57. Thoralf Skolem. Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre. In Matematikerkongressen i Helsingfors den 4-7 Juli 1922, Den femte skandinaviska matematikerkongressen, Redogorelse, pages 217-232. Akademiska Bokhandeln, 1923. Google Scholar
  58. Jan M. Smith. Propositional functions and families of types. Notre Dame Journal of Formal Logic, 30(3), 1989. URL: https://doi.org/10.1305/ndjfl/1093635159.
  59. Raymond M. Smullyan and Melvin Fitting. Set Theory and the Continuum Problem. Dover Books on Mathematics. Dover Publications, 2010. Google Scholar
  60. Kristina Sojakova. Higher Inductive Types as Homotopy-Initial Algebras. PhD thesis, Carnegie Mellon University, 2016. URL: http://ra.adm.cs.cmu.edu/anon/2016/abstracts/16-125.html.
  61. Raffael Stenzel. On univalence, Rezk completeness and presentable quasi-categories. PhD thesis, University of Leeds, 2019. URL: https://etheses.whiterose.ac.uk/id/eprint/24342.
  62. Thomas Streicher. Universes in toposes. In Laura Crosilla and Peter M. Schuster, editors, From sets and types to topology and analysis - Towards practicable foundations for constructive mathematics, volume 48 of Oxford Logic Guides. Oxford University Press, 2005. URL: https://doi.org/10.1093/acprof:oso/9780198566519.003.0005.
  63. Taichi Uemura. Colimits in the ∞-category of ∞-topoi and étale morphisms, 2025. URL: https://arxiv.org/abs/2506.10431.
  64. The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. URL: https://homotopytypetheory.org/book/, 2013.
  65. Benno van den Berg and Ieke Moerdijk. Univalent completion. Mathematische Annalen, 371:1337-1350, 2018. URL: https://doi.org/10.1007/s00208-017-1614-3.
  66. Niels van der Weide and Herman Geuvers. The construction of set-truncated higher inductive types. Electronic Notes in Theoretical Computer Science, 347:261-280, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.014.
  67. Jean van Heijenoort. From Frege to Gödel: A source book in mathematical logic, 1879-1931. Harvard University Press, 1967. Google Scholar
  68. Niccolò Veltri and Niels van der Weide. Constructing higher inductive types as groupoid quotients. Logical Methods in Computer Science, 17(2):8:1-8:42, 2021. URL: https://doi.org/10.23638/LMCS-17(2:8)2021.
  69. Vladimir Voevodsky. Univalent foundations project, 2010. Modified version of an NSF grant application. URL: http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf.
  70. Vladimir Voevodsky. Resizing Rules - their use and semantic justification, September 2011. Slides from a talk at TYPES 2011. URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf.
  71. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at http://unimath.org. URL: https://doi.org/10.5281/zenodo.10849216.
  72. John von Neumann. Zur Einführung der transfiniten Zahlen. Acta litterarum ac scientiarum Regiae Universitatis Hungaricae Francisco-Josephinae, Sectio scientiarum mathematicarum, 1:199-208, 1923. Google Scholar
  73. David Wärn. Eilenberg-Maclane spaces and stabilisation in homotopy type theory. Journal of Homotopy and Related Structures, 18:357-368, 2023. URL: https://doi.org/10.1007/s40062-023-00330-5.
  74. Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre. I. Mathematische Annalen, 65:261-281, 1908. URL: https://doi.org/10.1007/BF01449999.
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