Sökning: onr:"swepub:oai:research.chalmers.se:1fc7ee88-75c1-48dd-b6c1-893eedb611a5" >
Partial Univalence ...
Partial Univalence in n-truncated Type Theory
-
- Sattler, Christian, 1988 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Vezzosi, Andrea, 1986 (författare)
- IT-Universitetet i Kobenhavn,IT University of Copenhagen
-
(creator_code:org_t)
- 2020-07-08
- 2020
- Engelska.
-
Ingår i: ACM International Conference Proceeding Series. - New York, NY, USA : ACM. ; , s. 807-819
- Relaterad länk:
-
https://dl.acm.org/d...
-
visa fler...
-
https://doi.org/10.1...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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)