The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Does Coq support heterogenous relations for setoid rewriting?  In particular, I'm interested in the following version of [respectful]:

Definition respectful_partial_hetero {A B C D : Type}

  (R : A -> B -> Prop) (R' : C -> D -> Prop) : (A -> C) -> (B -> D) -> Prop :=

  Eval compute in @respectful_hetero A B (fun _ => C) (fun _ => D) R (fun _ _ => R').

My use case is that my types have indices, and I want to fix the indices being considered in the relation, but they don't have to be the same on each side.  Is there any way that I can make use of setoid rewriting for such heterogeneous relations?

Thanks,

Jason