Partial Univalence in n-truncated Type Theory

• 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.

Ämnesord

NATURVETENSKAP  -- Matematik -- Algebra och logik (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Algebra and Logic (hsv//eng)

NATURVETENSKAP  -- Matematik -- Geometri (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Geometry (hsv//eng)

NATURVETENSKAP  -- Matematik -- Matematisk analys (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Mathematical Analysis (hsv//eng)

Nyckelord

cubical type theory

homotopy type theory

univalence

Publikations- och innehållstyp

kon (ämneskategori)

ref (ämneskategori)