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öf dependent type theory,
and for some results assume further principles including function extensionality,
propositional extensionality, propositional truncation, and the univalence axiom.
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.
Original language | English |
---|---|
Title of host publication | Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016 |
Editors | Herman Geuvers, Jelena Ivetic, Silvia Ghilezan |
Publisher | Schloss Dagstuhl |
Number of pages | 15 |
ISBN (Electronic) | 9783959770651 |
DOIs | |
Publication status | Published - 1 Oct 2018 |
Event | 22nd International Conference on Types for Proofs and Programs, TYPES 2016 - Novi Sad, Serbia Duration: 23 May 2016 → 26 May 2016 |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Publisher | Dagstuhl Publishing |
ISSN (Electronic) | 1868-8969 |
Conference
Conference | 22nd International Conference on Types for Proofs and Programs, TYPES 2016 |
---|---|
Country/Territory | Serbia |
City | Novi Sad |
Period | 23/05/16 → 26/05/16 |
Bibliographical note
Funding Information:Supported by The United States Air Force Research Laboratory under agreement number FA9550-15-1-0053. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the United States Air Force Research Laboratory, the U.S. Government, or Carnegie Mellon University.
Publisher Copyright:
© Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman; licensed under Creative Commons License CC-BY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).
Keywords
- Relational parametricity
- dependent type theory
- univalent foundations
- homotopy type theory
- excluded middle
- classical mathematics
- constructive mathematics
ASJC Scopus subject areas
- Software