The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Arthur,

        you miss two things to make this work. First, you not only have
to show that every [Map f] is an eq-preserving function but that [Map]
itself is an eq-preserving operator, so as to be able to rewrite [Map  
f a1]
inside [Map (Map f a1) a2] for example.

Add Parametric Morphism (A B : Setoid) :
  (@Map A B) with signature (@map_equal A B ==> @eq A ==> @eq B)
  as setoid_mor.
Proof. intros f g Hfg x y Hxy. rewrite (Map_pres f x y Hxy). apply  
Hfg. Qed.

Secondly, you need to declare explicitely the Equivalence instance to  
the
typeclass system using:

Existing Instance map_equal_is_equivalence.

You have to do that even if you showed that every [Setoid] gives rise  
to an
[Equivalence] and declare your setoids as canonical structures: the two
mechanisms do not combine nicely (yet!).

-- Matthieu