LIPIcs.TYPES.2016.7.pdf
- Filesize: 453 kB
- 14 pages
Document
Parametricity, Automorphisms of the Universe, and Excluded Middle
Authors
-
Part of:
Volume:
22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-11-05
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)
https://doi.org/10.4230/LIPIcs.TYPES.2016.7
https://doi.org/10.4230/LIPIcs.TYPES.2016.7
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.
Keywords
- relational parametricity
- dependent type theory
- univalent foundations
- homotopy type theory
- excluded middle
- classical mathematics
- constructive mat
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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: http://dx.doi.org/10.1145/2535838.2535852.
- Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free: Parametricity for dependent types. J. Funct. Program., 22(2):107-152, 2012. URL: http://dx.doi.org/10.1017/S0956796812000056.
- Auke Booij. Agda development for "parametricity, automorphisms of the universe, and excluded middle", June 2017. URL: https://github.com/abooij/parametricityandlem-agda.
- Martín Hötzel Escardó. Automorphisms of U. Homotopy Type Theory mailing list, August 2014. URL: https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/blCo7x-B7aoJ.
- 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: http://dx.doi.org/10.1016/j.apal.2016.04.010.
- HoTT Project. The homotopy type theory Coq library. http://github.com/HoTT/HoTT/, 2015.
- 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: http://dx.doi.org/10.4230/LIPIcs.CSL.2012.381.
- Nicolai Kraus. Automorphisms of U. Homotopy Type Theory mailing list, August 2014. URL: https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/Phqpk7aMR7cJ.
- 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: http://dx.doi.org/10.23638/LMCS-13(1:15)2017.
- Dan Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. Logic in Computer Science (LICS), 2014. URL: http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf.
-
Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Lecture Notes. Bibliopolis, Naples, 1984.
-
John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513-523, 1983.
-
Egbert Rijke. The join construction. arXiv:1701.07538, 2017.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book.