theory.setoids

Require Import
  abstract_algebra.

Instance ext_equiv_trans `{Setoid A} `{Setoid B}: Transitive (_ : Equiv (A B)).

Instance ext_equiv_sym `{Setoid A} `{Setoid B}: Symmetric (_ : Equiv (A B)).

Instance: Equiv Prop := iff.
Instance: Setoid Prop := {}.

Lemma projected_setoid `{Setoid B} `{Equiv A} (f: A B)
  (eq_correct : x y, x = y f x = f y) : Setoid A.

Instance sig_Setoid `{Setoid A} (P: A Prop): Setoid (sig P).

Instance sigT_Setoid `{Setoid A} (P: A Type): Setoid (sigT P).

Definition prod_equiv `{Equiv A} `{Equiv B} : Equiv (A * B) := λ p q, fst p = fst q snd p = snd q.
Hint Extern 0 (Equiv (_ * _)) => eapply @prod_equiv : typeclass_instances.

Section simple_product.
  Context `{Setoid A} `{Setoid B}.

  Global Instance: Setoid (A * B) := {}.

  Global Instance pair_proper : Proper ((=) ==> (=) ==> (=)) (@pair A B).

  Global Instance: Setoid_Morphism (@fst A B).

  Global Instance: Setoid_Morphism (@snd A B).
End simple_product.

Section product.
  Context (I: Type) (c: I Type) `{ i, Equiv (c i)} `{ i, Setoid (c i)}.

  Let product: Type := i, c i.

  Instance product_equiv: Equiv product := `( i, x i = y i).

  Global Instance: Setoid product.

  Global Instance projection_morphism i: Setoid_Morphism (λ c: product, c i).
End product.

Instance id_morphism `{Setoid T}: Setoid_Morphism (@id T) := {}.

Instance compose_morphisms (A B C: Type)
  `{!Equiv A} `{!Equiv B} `{!Equiv C} (f: A B) (g: B C)
  {P: Setoid_Morphism f} {Q: Setoid_Morphism g}: Setoid_Morphism (g f).

Instance: `{Setoid_Morphism A B f} `{!Inverse f}, Bijective f Setoid_Morphism (f⁻¹).

Instance morphism_proper `{ea: Equiv A} `{eb: Equiv B}: Proper ((=) ==> (=)) (@Setoid_Morphism A B _ _).