# 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.