在直觉类型理论中，系统 LambdaP2 是否总是蕴含 CoC？

Question

考虑 lambda 立方体：

https://en.wikipedia.org/wiki/Lambda_cube

同时支持类型多态和依赖类型的类型系统：

• dependent type/type depending term:∀(a: A), B
• 类型多态性/术语取决于类型：∃ A, (b: B)

（假设 a,b,c 是项，A,B,C 是类型）

可归类为λP2系统，是二阶谓词逻辑的体现。

它的扩展，称为构造微积分 (CoC)，也支持：

• higher-kind/type-constructor/type depending on type: A -> B

它是大多数最强大的证明助手的基础，包括coq、LEAN3/4和agda。

这个额外的能力似乎没有用，因为任何这样的推论都可以重写成等价的对偶形式：

{ // primary
  A -> B
}

{ // dual
  ∃ A, (g: G)
  ∀ (g: G), B
}

在这里，术语

G

（将被称为通用对象）只是一个中间结构，携带很少的编译时信息，可以由证明者/编译器即时生成，并且可以在运行中擦除-时间。

那么为什么需要 CoC（或许多依赖类型系统中的更高级规则）？具体来说：

• 是否存在从 CoC 中的每个证明到 λP2 的单射映射？
• 鉴于依赖对象类型（DOT，Scala 3 的底层类型系统）系统是系统 D 的扩展，它类似于 λP2 但将依赖类型限制为路径显式、编译时已知术语，是否存在来自每个的单射映射Scala 程序到没有更高种类的等效程序？