pith. sign in

arxiv: 1701.05617 · v2 · pith:LV64UW7Jnew · submitted 2017-01-19 · 💻 cs.LO · math.LO

Parametricity, automorphisms of the universe, and excluded middle

classification 💻 cs.LO math.LO
keywords axiomsclassicaltypeassumingautomorphismsdependentextensionalitypropositional
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.