When dealing with equalities on types in Agda, it is often necessary to coerce the inhabitants the types using a hand-made coercion like
coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
coerce refl x = x
It was discussed here that explicit coercion of terms could sometimes be avoided using rewriting. I was wondering if this technique worked as well when defining types. So I wrote a little example where f,g : A → Set are two (extentionally) equal dependent types and a property p : A → Set where p x state that every element y : f x is equal to every element z : g x, that is y ≡ z. The last equality is ill-typed, as one can expect since y : f x and z : g x do not share the same type a priori, however I was hoping that rewriting could allow it. Something like:
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
But the error is still there, even though the rewrite advice is accepted. So, is there a way to make Agda accept this definition without using an explicit coercion, like
p {x} = (y : f x ) (z : g x) → (coerce f≡g y) ≡ z
?
Thank you
Here's a variation of your code that does what you want:
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
Why does this work when your version doesn't? rewrite affects two things: (a) the types of variables introduced in patterns left of the rewrite; (b) the goal type. If you look at your rewrite, when it takes effect, there is no f x to be found, so it does nothing. My rewrite, on the other hand, changes the type of fx : f x to g x because fx is introduced before the rewrite.
However, I would be surprised if this helped you much. In my experience, heterogeneous equality (i.e. equality between things of different types) remains annoying, regardless of what tricks you throw at it. For example, consider this variation of your idea, where we define a type R by rewriting:
R : ∀ {x} → f x → g x → Set
R {x} fx gx rewrite f≡g x = fx ≡ gx
R is a heterogenous relation which 'looks' reflexive. However, the closest we can come to stating reflexivity is
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
Without the coerce, fx would have the wrong type, and so we're back to the problem that we have these coercions polluting our types. This is not necessarily a deal breaker, but it complicates things. So, my advice is to avoid heterogeneous relations if possible.