The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I had fun with Equivalences today.

At first I made equivalence for functions.

Definition fun_equiv {A B} (f g: A -> B) := forall x y, x = y -> f x = g y.

Instance fun_Equiv {A B}: Equivalence (fun_equiv (A := A) (B := B)).
Proof.
 split; unfold fun_equiv.
  unfold Reflexive. congruence.
  unfold Symmetric. intros. symmetry. eauto.
  unfold Transitive. intros. pose (H _ _ H1). pose (H0 _ _ H1). congruence.
Defined.

Then I had idea of doing the same things for Proper.

Definition Proper_equiv {A B RA RB} (f g: A -> B) (FA: Proper (RA ==> RB) f) (FB: Proper (RA ==> RB) g)
 := forall x y, RA x y -> RB (f x) (g y).

After some time I understood why I can't make an Equivalence. It's because Proper_equiv isn't relation (FA and FB has different types).

Of course, I can make something like this and then further:

Structure morphism A B RA RB := {
 morphism_fun: A -> B;
 morphism_Proper: Proper (RA ==> RB) morphism_fun
}.

Have anyone encountered situation where such structure as 'morphism' had to be made?

I'm just fooling around with Equivalences, and the idea wasn't from any practical problems, so it is interesting for me if it has happened in serious developments.