Martin-Löf类型论中的匿名存在概念
计算机科学中的逻辑
2019-03-14 v2
摘要
正如Hofmann和Streicher的广群模型所证明的，内涵式Martin-Löf类型论中的身份证明通常不能被证明是唯一的。受Hedberg一个定理的启发，我们给出了确实具有唯一身份证明的类型的一些简单刻画。这些构造中的一个关键成分是身份类型上的弱常值自映射。我们研究任意类型上的此类自映射，并证明它们总是通过一个命题类型（即截断或压扁域）进行分解。对于一般的弱常值函数，这种分解是不可能的（Shulman的一个结果），但我们给出了几个可以实现分解的非平凡情形。基于这些结果，我们在类型论中定义了一种新的匿名存在概念，并仔细比较了不同的存在形式。此外，我们展示了截断的判断性计算规则可能带来的令人惊讶的后果，特别是在同伦类型论的背景下。所有结果已在依赖类型编程语言Agda中形式化并验证。
引用
@article{arxiv.1610.03346,
title = {Notions of Anonymous Existence in Martin-L\"of Type Theory},
author = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch},
journal= {arXiv preprint arXiv:1610.03346},
year = {2019}
}
备注
36 pages, to appear in the special issue of TLCA'13 (LMCS)