如何证明相等的函数类型具有相等的域？

Question

我想证明

\n\n

\xe2\x88\x80 {\xe2\x84\x93} {A B C D : Set \xe2\x84\x93} \xe2\x86\x92 (A \xe2\x86\x92 B) \xe2\x89\xa1 (C \xe2\x86\x92 D) \xe2\x86\x92 A \xe2\x89\xa1 C\n

\n\n

（与密码域类似）。

\n\n

如果我有一个函数domain返回函数类型域的函数，我可以将证明写为

\n\n

cong domain\n

\n\n

但我认为不可能编写这样的函数。

\n\n

有什么办法可以做到这一点吗？

\n

Answer 1

几个月前，我在 Agda 邮件列表上提出了一个非常类似的问题，请参阅： https: //lists.chalmers.se/pipermail/agda/2013/005787.html。简而言之，你无法在 Agda 中证明这一点。

\n

技术原因是 Agda 内部使用的用于模式匹配的统一算法不包括 形式问题的情况(A \xe2\x86\x92 B) \xe2\x89\xa1 (C \xe2\x86\x92 D)，因此此定义不进行类型检查：

\n

cong-domain : \xe2\x88\x80 {\xe2\x84\x93} {A B C D : Set \xe2\x84\x93} \xe2\x86\x92 (A \xe2\x86\x92 B) \xe2\x89\xa1 (C \xe2\x86\x92 D) \xe2\x86\x92 A \xe2\x89\xa1 C\ncong-domain refl = refl\n

\n

直接定义函数也是不可能的domain。想一想：非函数类型的类型的域应该是什么，例如Bool？

\n

无法证明这一点的更深层次原因是它与同伦类型理论的单价公理不相容。在 Guillaume Brunerie 在我的邮件中给出的答复中，他给出了以下示例：考虑两种类型Bool -> Bool和Unit -> (Bool + Bool)。两者都有 4 个元素，因此我们可以使用单价公理给出类型证明Bool -> Bool \xe2\x89\xa1 Unit -> (Bool + Bool)（实际上有 24 种不同的证明）。但显然我们不想Bool \xe2\x89\xa1 Unit！因此，在存在单价性的情况下，我们不能假设相同的函数类型具有相同的域。

\n

最后，我通过A \xe2\x89\xa1 C在需要的地方传递一个额外的类型参数来“解决”这个问题。我知道这并不理想，但也许你也可以这样做。

\n

我还应该注意到，Agda 确实包含单射类型构造函数的选项，您可以通过将其放在{-# OPTIONS --injective-type-constructors #-}.agda 文件的顶部来启用它。例如，这允许您证明A \xe2\x89\xa1 Bfrom List A \xe2\x89\xa1 List B，但不幸的是，这只适用于类型构造函数，例如List，而不适用于函数类型。

\n

当然，您始终可以在https://code.google.com/p/agda/issues/list--injective-function-types提出功能请求，以向 Agda添加选项。此选项与单价不兼容，但也是如此--injective-type-constructors，但对于许多应用程序来说，这不是一个真正的问题。我感觉Agda的主要开发者通常对这样的请求非常开放，并且非常快地将它们添加到Agda的开发版本中。

\n