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

Question

在处理 Agda 中类型的相等性时，通常需要使用像

这样的手工强制转换来强制居民使用类型

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

有人讨论有时可以使用重写来避免显式的术语强制转换。我想知道这种技术在定义类型时是否同样有效。所以我写了一个小例子，其中 f,g : A → Set 是两个（扩展）相等的依赖类型和一个属性 p : A → Set 其中 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 是在 rewrite.

之前引入的

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

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

R 是 'looks' 自反的异构关系。然而，我们可以得出的最接近自反性的说法是

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 就会有错误的类型，所以我们又回到了我们有这些强制转换污染我们的类型的问题。这不一定会破坏交易，但会使事情复杂化。所以，我的建议是尽可能避免异构关系。

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

Agda: rewriting instead of explicit coercion in type definition?

agda

coercion

rewriting