Parametricity, automorphisms of the universe, and excluded middle
(English)Manuscript (preprint) (Other academic)
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 in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
Algebra and Logic
Research subject Mathematical Logic
IdentifiersURN: urn:nbn:se:su:diva-140146OAI: oai:DiVA.org:su-140146DiVA: diva2:1077739