3

在 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

?

谢谢

4

1 回答 1

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是一种“看起来”是反身的异质关系。然而，我们能得出的最接近自反性的说法是

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

于 2019-02-08T19:08:14.550 回答