参数性、宇宙的自同构与排中律
计算机科学中的逻辑
2017-06-28 v2 逻辑
摘要
已知通过假设经典公理可构造非参数函数。我们的工作是其逆：我们在依赖类型论中通过假设非参数性的特定实例来证明经典公理。我们还探讨了经典公理与类型宇宙自同构存在性之间的相互作用。我们在内涵马丁-洛夫依赖类型论上工作，并在部分结果中进一步假设包括函数外延性、命题外延性、命题截断和单值公理等原理。
引用
@article{arxiv.1701.05617,
title = {Parametricity, automorphisms of the universe, and excluded middle},
author = {Auke Bart Booij and Martín Hötzel Escardó and Peter LeFanu Lumsdaine and Michael Shulman},
journal= {arXiv preprint arXiv:1701.05617},
year = {2017}
}
备注
15 pages, to appear in post-proceedings of TYPES 2016