我想证明
∀ {ℓ} {A B C D : Set ℓ} → (A → B) ≡ (C → D) → A ≡ C
（和codomain类似）。
如果我有一个domain返回函数类型域的函数，我可以将证明写为
cong domain
但我认为不可能写出这样的函数。
有没有办法做到这一点？
问问题
475 次
1 回答
3
几个月前，我在 Agda 邮件列表上提出了一个非常相似的问题，请参阅： http: //permalink.gmane.org/gmane.comp.lang.agda/5624。简短的回答是您无法在 Agda 中证明这一点。
技术原因是 Agda 内部用于模式匹配的统一算法不包括 form 问题的案例(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 ≡ Bfrom List A ≡ List B，但不幸的是，这仅适用于类型构造函数，例如List，而不适用于函数类型。
您当然可以随时在https://code.google.com/p/agda/issues/list--injective-function-types上提出功能请求，以向 Agda添加选项。此选项与单价不兼容，但也是如此--injective-type-constructors，但对于许多应用程序来说，这不是一个真正的问题。我觉得主要的 Agda 开发人员通常对这样的请求非常开放，并且很快将它们添加到 Agda 的开发版本中。
于 2014-01-26T11:01:11.090 回答