文章基本信息

标题：Parametricity, Automorphisms of the Universe, and Excluded Middle
本地全文：下载
作者：Auke B. Booij ; Mart{\'i}n H. Escard{\'o ; Peter LeFanu Lumsdaine 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：97
页码：1-14
DOI：10.4230/LIPIcs.TYPES.2016.7
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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