Parametricity, automorphisms of the universe, and excluded middle
From MaRDI portal
Publication:6282147
arXiv1701.05617MaRDI QIDQ6282147FDOQ6282147
Authors: Auke Bart Booij, Martín Escardo, Peter Lefanu Lumsdaine, Michael Shulman 
Publication date: 19 January 2017
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.
Has companion code repository: https://github.com/abooij/parametricityandlem-agda
This page was built for publication: Parametricity, automorphisms of the universe, and excluded middle
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6282147)
