Partial Univalence in n-truncated Type Theory

DOI10.1145/3373718.3394759zbMATH Open1498.03034arXiv2005.00260OpenAlexW3031831525MaRDI QIDQ5145682

Andrea Vezzosi, Christian Sattler

Publication date: 21 January 2021

Published in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous "partial" univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to $(n-1)$-types is consistent with the assumption that all types are $n$-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.

Full work available at URL: https://arxiv.org/abs/2005.00260

zbMATH Keywords

univalencehomotopy type theorycubical type theory

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (2)

On the \(n\)-uniqueness of types in rosy theories ⋮ Title not available (Why is that?)

This page was built for publication: Partial Univalence in n-truncated Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145682)