2026-07-30T14:03:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27028 2026-07-30T09:16:25Z ddc:004 open_access

Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations Cavallo, Evan Coquand, Thierry Homotopy type theory axiom of replacement univalent completion higher inductive type cubical sets 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Evan Cavallo and Thierry Coquand 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.10 urn:nbn:de:0030-drops-270286 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.10 eng https://creativecommons.org/licenses/by/4.0/legalcode