Booij, Auke B.
[VerfasserIn];
Escardó, Martín H.
[VerfasserIn];
Lumsdaine, Peter LeFanu
[VerfasserIn];
Shulman, Michael
[VerfasserIn]
;
Auke B. Booij and Martín H. Escardó and Peter LeFanu Lumsdaine and Michael Shulman
[MitwirkendeR]
Parametricity, Automorphisms of the Universe, and Excluded Middle
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and for some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.