是否有可能在简单不一致公理的结构演算中提取Sigma的第二个元素？

Question

它seems to be impossible在构造微积分中提取Sigma的第二个元素。而且，似乎没有已知的，简单的方法来扩展构造微积分，具有相关的抵消而不会失去一致性。因此，如何利用一个简单但不一致的公理（如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的存在，并断言相应的方程保持命题。

在简单的CoC中，我们说如果有一个类型的术语，两个术语x1和x2在命题上是相等的

forall T, T x1 -> T x2

（这有时被称为莱布尼茨平等：如果第一个持有的每个谓词都包含第二个，则两个术语相等。）对snd说类似更为复杂，因为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

Edit

关于你的评论：由于可兑换性通常不能用类型来表达，我们需要在类型理论中修改它的定义，使其具有带有第一和第二个投影的真正的sigma类型 - 比简单地假定某些公理所持有的更精细的操作。有一些系统允许这样做，例如Dedukti，一种在Inria开发的校样检查器。