Authors
Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, Michael Shulman
Abstract
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.
Keywords and phrases
relational parametricity, dependent type theory, univalent foundations,
homotopy type theory, excluded middle, classical mathematics, constructive mathematics