Parametricity, Automorphisms of the Universe, and Excluded Middle

Authors Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, Michael Shulman

Thumbnail PDF


  • Filesize: 453 kB
  • 14 pages

Document Identifiers

Author Details

Auke B. Booij
Martín H. Escardó
Peter LeFanu Lumsdaine
Michael Shulman

Cite AsGet BibTex

Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


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 for some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
  • relational parametricity
  • dependent type theory
  • univalent foundations
  • homotopy type theory
  • excluded middle
  • classical mathematics
  • constructive mat


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, San Diego, CA, USA, January 20-21, 2014, pages 503-516, 2014. URL:
  2. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free: Parametricity for dependent types. J. Funct. Program., 22(2):107-152, 2012. URL:
  3. Auke Booij. Agda development for "parametricity, automorphisms of the universe, and excluded middle", June 2017. URL:
  4. Martín Hötzel Escardó. Automorphisms of U. Homotopy Type Theory mailing list, August 2014. URL:
  5. Martín Hötzel Escardó and Thomas Streicher. The intrinsic topology of Martin-Löf universes. Ann. Pure Appl. Logic, 167(9):794-805, 2016. URL:
  6. HoTT Project. The homotopy type theory Coq library., 2015.
  7. Chantal Keller and Marc Lasson. Parametricity in an impredicative sort. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, pages 381-395, 2012. URL:
  8. Nicolai Kraus. Automorphisms of U. Homotopy Type Theory mailing list, August 2014. URL:
  9. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, 13(1), 2017. URL:
  10. Dan Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. Logic in Computer Science (LICS), 2014. URL:
  11. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Lecture Notes. Bibliopolis, Naples, 1984. Google Scholar
  12. John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513-523, 1983. Google Scholar
  13. Egbert Rijke. The join construction. arXiv:1701.07538, 2017. Google Scholar
  14. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail