教会编码的依赖对

Question

人们可以很容易地教会编码这样的对：

Definition prod (X Y:Set) : Set := forall (Z : Set), (X -> Y -> Z) -> Z.

Definition pair (X Y:Set)(x:X)(y:Y) : prod X Y := fun Z xy => xy x y.

Definition pair_rec (X Y Z:Set)(p:X->Y->Z) (xy : prod X Y) : Z := xy Z p.

Definition fst (X Y:Set)(xy:prod X Y) : X := pair_rec X Y X (fun x y => x) xy.

Definition snd (X Y:Set)(xy:prod X Y) : Y := pair_rec X Y Y (fun x y => y) xy.

然后很容易将它概括为依赖对，如下所示：

Definition dprod (X:Set)(Y:X->Set) : Set :=
forall (Z : Set), (forall (x:X),Y x->Z)->Z.

Definition dpair (X:Set)(Y:X->Set)(x:X)(y:Y x) : dprod X Y :=
fun Z xy => xy x y.

Definition dpair_rec (X:Set)(Y:X->Set)(Z:Set)(p:forall (x:X),Y x->Z)
(xy : dprod X Y) : Z := xy Z p.

Definition dfst (X:Set)(Y:X->Set)(xy:dprod X Y) : X :=
dpair_rec X Y X (fun x y => x) xy.

Definition dsnd (X:Set)(Y:X->Set)(xy:dprod X Y) : Y (dfst X Y xy) :=
dpair_rec X Y (Y (dfst X Y xy)) (fun x y => y) xy.

但是，最后一个定义失败并显示错误消息：

In environment
X : Set
Y : X -> Set
xy : dprod X Y
x : X
y : Y x
The term "y" has type "Y x"
while it is expected to have type 
"Y (dfst X Y xy)".

我在这里理解这个问题。但是解决方案是什么？换句话说，如何教会编码依赖对？

Answer 1

首先，让我们把术语说得对。

你所谓的dprod实际上是一个“依赖和”，而“依赖产品”就是你可能想要称之为“依赖函数”的东西。这样做的原因是依赖函数概括了常规产品，你只需巧妙地使用Bool：

prod : Set -> Set -> Set
prod A B = (b : Bool) -> case b of { True -> A; False -> B; }
{-
The type-theoretic notation would be:
prod A B = Π Bool (\b -> case b of { True -> A; False -> B; })
-}

mkPair : (A B : Set) -> A -> B -> prod A B
mkPair A B x y = \b -> case b of { True -> x; False -> y; }

elimProd : (A B Z : Set) -> (A -> B -> Z) -> prod A B -> Z
elimProd A B Z f p = f (p True) (p False)

同样的精神，依赖对（通常表示为Σ）概括了常规总和：

sum : Set -> Set -> Set
sum A B = Σ Bool (\b -> case b of { True -> A; False -> B; })

mkLeft : (A B : Set) -> A -> sum A B
mkLeft A B x = (True, x)

mkRight : (A B : Set) -> B -> sum A B
mkRight A B y = (False, y)

elimSum : (A B Z : Set) -> (A -> Z) -> (B -> Z) -> sum A B -> Z
elimSum A B Z f _ (True, x) = f x
elimSum A B Z _ g (False, y) = g y

这可能令人困惑，但另一方面，Π A (\_ -> B)是常规函数的类型，而Σ A (\_ -> B)是常规对的类型（例如，参见here）。

所以，再一次：

• 依赖产品=依赖函数的类型
• 从属和=从属对的类型

---

您的问题可以通过以下方式重新定义：

通过依赖产品是否存在针对依赖和的教会编码？

之前已经在Math.StackExchange上询问过，这里的an answer与你的编码基本相同。

但是，阅读这个答案的评论，你会发现它显然缺乏预期的归纳原则。还有一个类似的问题，但关于教会编码的自然数，this answer（特别是评论）有点解释为什么Coq或Agda不足以推导归纳原理，你需要额外的假设，如参数。还有另外一个类似的question on MathOverflow，虽然对于Agda / Coq的具体情况答案没有明确的“是”或“否”，但它们暗示它可能是不可能的。

最后，我不得不提一下，就像现在的许多其他类型理论问题一样，显然是HoTT is the answer。引用Mike Shulman撰写博客文章的开头：

在这篇文章中，我将论证，改进Awodey-Frey-Speight的先前工作，（更高的）归纳类型可以使用具有完全依赖归纳原理的impredicative编码来定义 - 特别是，在没有任何截断假设的情况下消除所有类型的家族 - 普通的（令人印象深刻的）Book HoTT没有任何进一步的钟声或口哨声。

（虽然您将获得的（impredicative）编码很难称为Church编码。）

Answer 2

在Coq或Agda中没有教会编码依赖对的方法。

好吧，当我们想到同质元组AxA时，这也可以被理解为函数2 -> A。这也适用于使用依赖函数Pi x:2.if x then A else B的AxB等异构元组。然而，下一个逻辑步骤是Sigma x:A.B x，它没有作为函数的良好表示（除非我们接受非常依赖的函数，在我看来它违背了类型理论的精神）。由于这个原因，在我看来，从->到Pi以及从x到Sigma的推广是主要的，并且元组可以表示为函数的事实是次要的。 - Thorsten Altenkirch博士，在Agda邮件列表的某个地方

Thorsten提到的非常依赖的函数编码可以找到here（请注意，这不是有效的Agda，只是类似Agda的语法的“疯狂依赖”类型理论）。