Parametricity, automorphisms of the universe, and excluded middle

TL;DR

This paper explores the relationship between parametricity, classical axioms, and automorphisms of the universe within dependent type theory, showing how non-parametricity can imply classical principles.

Contribution

It demonstrates that classical axioms can be derived from specific instances of non-parametricity and investigates their interaction with universe automorphisms in dependent type theory.

Findings

Classical axioms can be derived assuming non-parametricity.

Automorphisms of the universe relate to classical principles.

Results depend on principles like univalence and propositional extensionality.

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.