Diaconescu定理是否暗示立方类型论非构造性？相关推导存疑

你的困惑其实源于对**两种不同“选择公理”**的混淆，以及类型论和集合论中“构造性”概念的细微差别——咱们一步步拆解清楚：

首先得明确：Martin-Löf类型论（MLTT）里的“选择公理”和集合论里的选择公理根本不是一回事：

• 在MLTT的“命题作为类型”框架下，所谓的“选择公理”（我们叫它类型论选择公理ACₜ）是可直接构造证明的：如果对每个x:X，你都能找到一个a:A(x)（对应类型Πx:X. Σa:A(x)的元素），那只要把每个x映射到对应的a（用λx. proj₁(f x)就能构造），就得到了函数f:Πx:A(x)。这完全是构造性的——你能显式写出选择函数，根本不存在集合论里那种“无法明确构造”的情况。

然后看Diaconescu定理：它说的是在构造性集合论中，集合论版本的选择公理（即对非空子集族选元素的那种，对应类型论里的“命题选择公理ACₚ”）会蕴含排中律。但这个定理的前提是“选择公理针对的是命题（即只有真/假两个状态的断言）”，而不是MLTT里的任意类型。

那回到立方类型论：

• 它确实是MLTT的扩展，所以自然能证明ACₜ——这和构造性完全不冲突，因为ACₜ本身就是构造性的。
• 你提到立方类型论能证明“内涵性”（其实准确来说是函数外延性：若对所有x，f x = g x则f = g），这是因为立方类型论的路径类型（同伦类型论的核心）天然支持函数之间的同伦等价作为相等性。但这并不会触发Diaconescu定理的问题，原因很简单：
  立方类型论并没有默认包含命题选择公理ACₚ——ACₚ是针对“命题截断”（即被抽象成“可居住/不可居住”的类型，无法从中提取具体元素）的选择，它不是立方类型论的定理，而是需要额外添加的非构造性公理。而ACₜ和函数外延性的组合，完全不会推出排中律，也不会破坏构造性。

简单来说，你的误解核心是把“类型论中可构造证明的选择公理”和“集合论中会导致排中律的选择公理”混为一谈了。立方类型论依然是构造性的——它保留了MLTT的构造性核心，只是通过同伦/路径类型扩展了相等性的表达，而函数外延性是这个扩展的自然结果，和Diaconescu定理的适用场景无关。

内容的提问来源于stack exchange，提问作者prover