是否有可能在具有简单不一致公理的构造演算中提取西格玛的第二个元素？

Question

这似乎是不可能提取西格玛在第二元件上构式的演算。此外，似乎没有已知的简单方法可以在不失去一致性的情况下扩展具有依赖消除的构造演算。因此，如何利用一个简单但不一致的公理（例如Type : Type或不受限制的递归，例如?）来提取 Sigma 的第二个元素？

也就是说，给定以下 Sigma 构造函数：

Sigma =
  ? A : *
  ? B : A -> *
  ? a : A
  ? b : B
  ? Data : *
  ? Sigma :
    ? fst : A
    ? snd : B fst
    Data
  Sigma a b

在等价于构造演算的语言中，除了使用Type : Type或其他一些简单的不一致公理外，是否有可能实现一个函数，给定一个项，如Sigma Nat (\x -> Nat) 3 6，提取第二个值，6？

Answer 1

在诸如 Martin-Löf 类型理论或结构演算之类的类型理论的上下文中，“不一致”我们通常指的是逻辑不一致：能够导出contra类型的术语forall T : Type, T。在这种情况下，任何其他类型都会T有人居住：适用contra于它就足够了。

不幸的是，在大多数类型理论中，有人居住并没有告诉我们可转换性或定义相等性，因为没有类型表示这两个术语x和y是可转换的。这意味着无法推导出术语

fst : Sigma A B -> A
snd : forall s : Sigma A B, B (fst s)

这样fst (Sigma _ _ x y)简化了x和snd (Sigma _ _ x y) 简化了y诉诸逻辑上的矛盾。（我滥用符号位，并使用Sigma该构造函数和类型都有了）你可以，但是，使用contra以假定的存在fst和snd并断言相应的等式成立propositionally。

在普通的行为准则，我们说两个词x1，并x2为propositionally等于如果有类型的术语

forall T, T x1 -> T x2

（这有时被称为莱布尼茨等式：如果第一个项的每个谓词都成立第二个项，则两个项是相等的。）声明一个相似的 forsnd稍微复杂一些，因为snd (Sigma _ _ x y)和y没有相同的类型（前者是类型B (fst (Sigma _ _ x y))，而后者是类型B x）。我们可以通过同时为fst和断言简化引理来解决这个问题snd：

forall (T : forall x : A, B x -> Type),
  T (fst (Sigma _ _ x y)) (snd (Sigma _ _ x y)) -> 
  T x y

编辑

关于您的评论：由于通常不能用类型来表达可转换性，我们需要修改它在类型理论中的定义，以获得具有第一和第二投影的真正 sigma 类型——比简单地假设某些公理成立更微妙的操作。有一些系统允许这样做，例如Dedukti，一种在 Inria 开发的证明检查器。