Parametricity, automorphisms of the universe, and excluded middle
Logic in Computer Science
2017-06-28 v2 Logic
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\"of dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
Keywords
Cite
@article{arxiv.1701.05617,
title = {Parametricity, automorphisms of the universe, and excluded middle},
author = {Auke Bart Booij and Martín Hötzel Escardó and Peter LeFanu Lumsdaine and Michael Shulman},
journal= {arXiv preprint arXiv:1701.05617},
year = {2017}
}
Comments
15 pages, to appear in post-proceedings of TYPES 2016