Partial univalence in n-truncated type theory

DOI10.1145/3373718.3394759MaRDI QIDQ5145682zbMATH OpenOpenAlexFDO

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)

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)

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.

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

Cited in

(7)

• Functions out of higher truncations
• The general universal property of the propositional truncation
• Higher homotopies in a hierarchy of univalent universes
• Stack semantics of type theory
• scientific article; zbMATH DE number 3983152 (Why is no real title available?)
• On the \(n\)-uniqueness of types in rosy theories
• Partial elements and recursion via dominances in univalent type theory

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)