2026-08-16T20:08:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10054 2024-03-06T10:42:59Z ddc:004 open_access

Decomposing the Univalence Axiom Orton, Ian Pitts, Andrew M. dependent type theory homotopy type theory univalent type theory univalence cubical type theory cubical sets This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ian Orton and Andrew M. Pitts 2019 Is Part Of LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2017.6 urn:nbn:de:0030-drops-100546 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.6 eng https://creativecommons.org/licenses/by/3.0/legalcode