Martin-Löf类型论中的匿名存在概念
Notions of Anonymous Existence in Martin-Löf Type Theory
摘要：
正如霍夫曼和施特赖歇的群胚模型所证明的那样，内涵马丁-洛夫类型论中的恒等式证明一般不能被证明是唯一的。受Hedberg的一个定理的启发，我们给出了一些简单的类型的特征，这些类型具有唯一的恒等式证明。这些构造中的一个关键成分是单位元类型上的弱常数内函数。我们研究这样的内函数的任意类型，并表明，他们总是通过一个命题类型，截断或压扁域的因素。这样的因式分解是不可能的弱常数函数一般（结果由舒尔曼），但我们提出了几个非平凡的情况下，它可以做到。基于这些结果，我们在类型论中定义了匿名存在的新概念，并仔细比较了不同形式的存在。此外，我们可能会令人惊讶的后果的判断计算规则的截断，特别是在同伦类型论的背景下。所有的结果已被形式化，并在依赖类型的程序设计语言Agda验证。
英文摘要：
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
