一句话：刻画具有唯一恒等证明的类型，基于弱常值自函数与命题截断提出匿名存在概念，并在 Agda 中验证。
论文研究内涵 Martin-Löf 类型论中恒等证明一般不唯一的问题，受 Hedberg 定理启发，给出具有唯一恒等证明的类型的简单刻画。核心工具是恒等类型上的弱常值自函数：作者证明这类函数总能通过一个命题类型（即截断/压缩后的定义域）分解，并指出一般弱常值函数并不具备该性质（Shulman 的结果），但给出若干可分解的非平凡情形。基于这些结果，论文定义了一种新的匿名存在概念，并仔细比较不同存在形式；还展示了截断的判定计算规则在同伦类型论中的一些可能令人意外的推论。所有结果均在依赖类型编程语言 Agda 中形式化验证。
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda.Comment: 36 pages, to appear in the special issue of TLCA'13 (LMCS)
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KrausECA16,
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 = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:15)2017}
}