2026-07-24T01:44:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9855 2024-03-06T10:42:24Z ddc:004 open_access

Parametricity, Automorphisms of the Universe, and Excluded Middle Booij, Auke B. Escardó, Martín H. Lumsdaine, Peter LeFanu Shulman, Michael relational parametricity dependent type theory univalent foundations homotopy type theory excluded middle classical mathematics constructive mat 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Auke B. Booij and Martín H. Escardó and Peter LeFanu Lumsdaine and Michael Shulman 2018 Is Part Of LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2016.7 urn:nbn:de:0030-drops-98554 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.7 eng https://creativecommons.org/licenses/by/3.0/legalcode