似乎不可能在构造微积分上提取Sigma的第二个元素。此外，似乎没有已知的简单方法可以通过依赖消除来扩展构造微积分而不会失去一致性。因此，如何利用简单但不一致的公理(如Type : Type或无限制递归，如μ)来提取西格玛的第二个元素？
也就是说，给定以下 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？
在类型论(如马丁-勒夫类型论或构造演算)的上下文中，"不一致"通常是指逻辑不一致：能够推导出类型forall T : Type, T的项contra。 在这种情况下，任何其他类型的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
编辑
关于你的评论：由于可转换性通常不能用类型来表达，我们需要修改它在类型论中的定义，以获得具有第一和第二投影的真西格玛类型——这是一个比简单地假设某些公理成立更微妙的操作。 有一些系统允许这样做，例如Dedukti，Inria开发的证明检查器。