Parametricity, automorphisms of the universe, and excluded middle

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

Parametricity, automorphisms of the universe, and excluded middle. / Booij, Auke; Escardo, Martin; Lumsdaine, Peter Lefanu ; Shulman, Michael .

Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016. Schloss Dagstuhl, 2017. (Leibniz International Proceedings in Informatics (LIPIcs)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Booij, A, Escardo, M, Lumsdaine, PL & Shulman, M 2017, Parametricity, automorphisms of the universe, and excluded middle. in Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016. Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl, 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, 23/05/16. <https://arxiv.org/pdf/1701.05617.pdf>

APA

Booij, A., Escardo, M., Lumsdaine, P. L., & Shulman, M. (2017). Parametricity, automorphisms of the universe, and excluded middle. In Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016 (Leibniz International Proceedings in Informatics (LIPIcs)). Schloss Dagstuhl. https://arxiv.org/pdf/1701.05617.pdf

Vancouver

Booij A, Escardo M, Lumsdaine PL, Shulman M. Parametricity, automorphisms of the universe, and excluded middle. In Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016. Schloss Dagstuhl. 2017. (Leibniz International Proceedings in Informatics (LIPIcs)).

Author

Booij, Auke ; Escardo, Martin ; Lumsdaine, Peter Lefanu ; Shulman, Michael . / Parametricity, automorphisms of the universe, and excluded middle. Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016. Schloss Dagstuhl, 2017. (Leibniz International Proceedings in Informatics (LIPIcs)).

Bibtex

@inproceedings{d2b2fa7c32c34e43b7ee10c3a40bde78,
title = "Parametricity, automorphisms of the universe, and excluded middle",
abstract = "It is known that one can construct non-parametric functions by assuming classicalaxioms. Our work is a converse to that: we prove classical axioms in dependenttype theory assuming specific instances of non-parametricity. We also addressthe interaction between classical axioms and the existence of automorphisms ofa type universe. We work over intensional Martin-L{\"o}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 mathematics",
author = "Auke Booij and Martin Escardo and Lumsdaine, {Peter Lefanu} and Michael Shulman",
year = "2017",
month = jun,
day = "27",
language = "English",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl",
booktitle = "Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016",
address = "Germany",
note = "22nd International Conference on Types for Proofs and Programs, TYPES 2016 ; Conference date: 23-05-2016 Through 26-05-2016",

}

RIS

TY - GEN

T1 - Parametricity, automorphisms of the universe, and excluded middle

AU - Booij, Auke

AU - Escardo, Martin

AU - Lumsdaine, Peter Lefanu

AU - Shulman, Michael

PY - 2017/6/27

Y1 - 2017/6/27

N2 - It is known that one can construct non-parametric functions by assuming classicalaxioms. Our work is a converse to that: we prove classical axioms in dependenttype theory assuming specific instances of non-parametricity. We also addressthe interaction between classical axioms and the existence of automorphisms ofa 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.

AB - It is known that one can construct non-parametric functions by assuming classicalaxioms. Our work is a converse to that: we prove classical axioms in dependenttype theory assuming specific instances of non-parametricity. We also addressthe interaction between classical axioms and the existence of automorphisms ofa 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.

KW - Relational parametricity

KW - dependent type theory

KW - univalent foundations

KW - homotopy type theory

KW - excluded middle

KW - classical mathematics

KW - constructive mathematics

UR - http://www.types2016.uns.ac.rs/index.php/2-uncategorised/21-post-proceedings

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

BT - Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016

PB - Schloss Dagstuhl

T2 - 22nd International Conference on Types for Proofs and Programs, TYPES 2016

Y2 - 23 May 2016 through 26 May 2016

ER -