Partial univalence in n-truncated type theory

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

Authors: 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

Recommendations

• Higher homotopies in a hierarchy of univalent universes
• scientific article; zbMATH DE number 6694181
• The simplicial model of univalent foundations (after Voevodsky)
• The univalence axiom in cubical sets
• Univalence for inverse diagrams and homotopy canonicity

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)

Cited In (7)

• Stack semantics of type theory
• Functions out of higher truncations
• The general universal property of the propositional truncation
• Partial elements and recursion via dominances in univalent type theory
• Title not available (Why is that?)
• On the \(n\)-uniqueness of types in rosy theories
• Higher homotopies in a hierarchy of univalent universes

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)