The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  This situation appears as soon as you work with setoids. What morphism defines is a morphism of setoids. See eg the math classes library for a modern library working with setoids, or the old concat library for a use in the context of categories if that's what you're into.

Best,
-- Matthieu

Le jeu. 2 juil. 2015 à 06:29, Christopher Ernest Sally <christopherernestsally AT gmail.com> a écrit :

Hi Ilmars

Hmm... what about comparison functions on finite partial maps of different values (but similar keys)?

Best

Chris

On 2 July 2015 at 02:12, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

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.