theory.strong_setoids

Require Import abstract_algebra.

Section contents.
Context `{StrongSetoid A}.

Global Instance: Setoid A.

Global Instance apart_proper: Proper ((=) ==> (=) ==> iff) (⪥).

Instance apart_ne x y : PropHolds (x y) PropHolds (x y).

Global Instance: x y, Stable (x = y).
End contents.

Hint Extern 3 (PropHolds (_ _)) => eapply @apart_ne : typeclass_instances.

Lemma projected_strong_setoid `{StrongSetoid B} `{Equiv A} `{Apart A} (f: A B)
  (eq_correct : x y, x = y f x = f y) (apart_correct : x y, x y f x f y) : StrongSetoid A.

Instance sig_strong_setoid `{StrongSetoid A} (P: A Prop): StrongSetoid (sig P).

Section morphisms.
  Context `{Equiv A} `{Apart A} `{Equiv B} `{Apart B} `{Equiv C} `{Apart C}.


  Global Instance strong_morphism_proper `{!StrongSetoid_Morphism (f : A B)} :
    Setoid_Morphism f | 10.

  Global Instance strong_injective_injective `{!StrongInjective (f : A B)} :
    Injective f.

  Global Instance strong_setoid_morphism_1 `{!StrongSetoid_BinaryMorphism (f : A B C)} :
     z, StrongSetoid_Morphism (f z).

  Global Instance strong_setoid_morphism_unary_2 `{!StrongSetoid_BinaryMorphism (f : A B C)} :
     z, StrongSetoid_Morphism (λ x, f x z).

  Lemma strong_binary_setoid_morphism_both_coordinates
    `{!StrongSetoid A} `{!StrongSetoid B} `{!StrongSetoid C} {f : A B C}
    `{ z, StrongSetoid_Morphism (f z)} `{ z, StrongSetoid_Morphism (λ x, f x z)} : StrongSetoid_BinaryMorphism f.

  Global Instance binary_strong_morphism_proper `{!StrongSetoid_BinaryMorphism (f : A B C)} :
    Proper ((=) ==> (=) ==> (=)) f.
End morphisms.

Section more_morphisms.
  Context `{StrongSetoid A} `{StrongSetoid B}.

  Lemma strong_binary_setoid_morphism_commutative {f : A A B} `{!Commutative f}
    `{ z, StrongSetoid_Morphism (f z)} : StrongSetoid_BinaryMorphism f.
End more_morphisms.

Global Instance default_apart `{Equiv A} : Apart A | 20 := (≠).
Typeclasses Opaque default_apart.

Global Instance default_apart_trivial `{Equiv A} : TrivialApart A (ap:=default_apart).

Section dec_setoid.
  Context `{Setoid A} `{Apart A} `{!TrivialApart A} `{ x y, Decision (x = y)}.

  Instance ne_apart x y : PropHolds (x y) PropHolds (x y).

  Instance dec_strong_setoid: StrongSetoid A.
End dec_setoid.

Section dec_setoid_morphisms.
  Context `{StrongSetoid A} `{!TrivialApart A} `{StrongSetoid B}.

  Instance dec_strong_morphism (f : A B) `{!Setoid_Morphism f} :
    StrongSetoid_Morphism f.

  Context `{!TrivialApart B}.

  Instance dec_strong_injective (f : A B) `{!Injective f} :
    StrongInjective f.

  Context `{StrongSetoid C}.

  Instance dec_strong_binary_morphism (f : A B C) `{!Proper ((=) ==> (=) ==> (=)) f} :
    StrongSetoid_BinaryMorphism f.
End dec_setoid_morphisms.