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

Question

我想证明

∀ {ℓ} {A B C D : Set ℓ} → (A → B) ≡ (C → D) → A ≡ C

（与共域类似）。

如果我有一个函数

domain

返回函数类型的域，我可以将证明写为

cong domain

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

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

Answer 1

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

技术原因是 Agda 内部使用的用于模式匹配的统一算法不包括

(A → B) ≡ (C → D)

形式的问题，因此该定义不进行类型检查：

cong-domain : ∀ {ℓ} {A B C D : Set ℓ} → (A → B) ≡ (C → D) → A ≡ C
cong-domain refl = refl

也不可能直接定义函数

domain

。想一想：非函数类型的类型的域应该是什么，例如

Bool

？

无法证明这一点的更深层次原因是它与同伦类型理论的单价公理不相容。在 Guillaume Brunerie 在我的邮件中给出的答复中，他给出了以下示例：考虑两种类型

Bool -> Bool

和

Unit -> (Bool + Bool)

。两者都有 4 个元素，因此我们可以使用一价公理给出

Bool -> Bool ≡ Unit -> (Bool + Bool)

类型的证明（实际上有 24 种不同的证明）。但显然我们不想要

Bool ≡ Unit

！因此，在存在单价性的情况下，我们不能假设相同的函数类型具有相同的域。

最后，我通过在需要的地方传递一个

A ≡ C

类型的额外参数来“解决”了这个问题。我知道这并不理想，但也许你也可以这样做。

我还应该注意到，Agda 确实包含单射类型构造函数的选项，您可以通过将

{-# OPTIONS --injective-type-constructors #-}

放在 .agda 文件的顶部来启用该选项。例如，这允许您从

A ≡ B

证明

List A ≡ List B

，但不幸的是，这只适用于类型构造函数，例如

List

，而不适用于函数类型。

您当然可以随时在 https://code.google.com/p/agda/issues/list 提出功能请求，以向 Agda 添加选项

--injective-function-types

。此选项与单价不兼容，但

--injective-type-constructors

也是如此，但对于许多应用程序来说，这不是一个真正的问题。我感觉Agda的主要开发者通常对这样的请求非常开放，并且非常快地将它们添加到Agda的开发版本中。