Agda:在类型定义中重写而不是显式强制转换？

Question

在处理 Agda 中类型的相等性时，通常需要使用像这样的手工强制来强制居民类型

coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
coerce refl x = x

讨论了here有时可以使用重写来避免明确的术语强制。我想知道这种技术在定义类型时是否同样有效。所以我写了一个小例子，其中 f,g : A → Set 是两个(extentionally)相等的依赖类型和一个属性 p : A → Set where p x 声明每个元素 y : f x 等于每个元素 z : g x，即 y ≡ z。最后一个等式是错误类型的，正如人们所预料的那样，因为 y : f x 和 z : g x 不共享相同的先验类型，但是我希望重写可以允许它。像这样的东西:

open import Relation.Binary.PropositionalEquality

postulate A : Set
postulate B : Set
postulate f : A → Set
postulate g : A → Set
postulate f≡g : ∀ {x} → (f x) ≡ (g x)

p : {x : A} → Set
p {x} rewrite f≡g {x} = (y : f x ) (z : g x) → y ≡ z

但错误仍然存​​在，即使重写建议被接受。那么，有没有办法让 Agda 在不使用显式强制转换的情况下接受这个定义，比如

p {x} = (y : f x ) (z : g x) → (coerce f≡g y) ≡ z

?

谢谢

Answer 1

这是您的代码的变体，可以满足您的需求:

open import Relation.Binary.PropositionalEquality

postulate
  A : Set
  f : A → Set
  g : A → Set
  f≡g : ∀ x → f x ≡ g x

p : (x : A) → Set
p x = ∀ y z → R y z
  where
    R : f x → g x → Set
    R fx gx rewrite f≡g x = fx ≡ gx

---

为什么您的版本不起作用？ rewrite 影响两件事:(a) 在 rewrite 左侧的模式中引入的变量类型； (b) 目标类型。如果您查看您的rewrite，当它生效时，没有f x 可以找到，所以它什么都不做。另一方面，我的 rewrite 将 fx : f x 的类型更改为 g x 因为之前引入了 fx 重写。

---

但是，如果这对您有很大帮助，我会感到很惊讶。根据我的经验，异构相等(即不同类型的事物之间的相等)仍然很烦人，不管你用什么技巧。例如，考虑您想法的这种变体，我们通过重写定义类型 R:

R : ∀ {x} → f x → g x → Set
R {x} fx gx rewrite f≡g x = fx ≡ gx

R 是一种“看起来”自反的异构关系。然而，我们可以得出的最接近自反性的说法是

coerce : {A B : Set} → A ≡ B → A → B
coerce refl x = x

R-refl : ∀ {x} {fx : f x} → R fx (coerce (f≡g x) fx)
R-refl {x} rewrite f≡g x = refl

如果没有 coerce，fx 就会有错误的类型，所以我们又回到了我们的问题，即这些强制转换污染了我们的类型。这不一定会破坏交易，但会使事情复杂化。因此，我的建议是尽可能避免异构关系。