Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Browse files

Generalize ext_equiv_trans and ext_equiv_sym.

We don't need the source and target to be Setoids, so just use
the weaker requirement.
  • Loading branch information...
commit 52be92a0b4613483161279c88132b440eac90136 1 parent 8e27adb
@tomprince tomprince authored
Showing with 2 additions and 2 deletions.
  1. +2 −2 src/theory/setoids.v
4 src/theory/setoids.v
@@ -4,10 +4,10 @@ Require Import
Lemma ext_equiv_refl `{Setoid_Morphism A B f} : f = f.
Proof. intros ?? E. pose proof (setoidmor_b f). now rewrite E. Qed.
-Instance ext_equiv_trans `{Setoid A} `{Setoid B} : Transitive (_ : Equiv (A → B)).
+Instance ext_equiv_trans `{Equiv A} `{Equiv B} `{Reflexive (A:=A) (=)} `{Transitive (A:=B) (=)} : Transitive (_ : Equiv (A → B)).
Proof. intros ? y ???? w ?. transitivity (y w); firstorder. Qed.
-Instance ext_equiv_sym `{Setoid A} `{Setoid B} : Symmetric (_ : Equiv (A → B)).
+Instance ext_equiv_sym `{Equiv A} `{Equiv B} `{Symmetric (A:=A) (=)} `{Symmetric (A:=B) (=)}: Symmetric (A:=A→B) (=).
Proof. firstorder. Qed.
Lemma ext_equiv_applied `{Setoid A} `{Equiv B} {f g : A → B} :

0 comments on commit 52be92a

Please sign in to comment.
Something went wrong with that request. Please try again.