The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hello,

I wonder if someone can point me to existing formalizations, if any, of heterogeneous relations in Coq (that is, A -> B -> Prop where A B : Type). In particular, I'm interested in left and right residuals, and also in symmetric quotients. Most of the formalizations that I looked at in the Standard Library are about homogeneous relations (that is, A -> A - Prop). Any pointers are greatly appreciated.

Thanks,
Lucian