# Library ConCaT.SETOID.Setoid

Require Export Relations.

Set Implicit Arguments.
Unset Strict Implicit.

Structure > Setoid : Type :=
{Carrier :> Type; Equal : Relation Carrier; Prf_equiv :> Equivalence Equal}.

Infix "=_S" := Equal (at level 70).

Lemma Refl : forall (S : Setoid) (x : S), x =_S x.
Proof.
intro S; exact (Prf_refl S).
Qed.

Lemma Sym : forall (S : Setoid) (x y : S), x =_S y -> y =_S x.
Proof.
intro S; exact (Prf_sym S).
Qed.

Lemma Trans : forall (S : Setoid) (x y z : S), x =_S y -> y =_S z -> x =_S z.
Proof.
intro S; exact (Prf_trans S).
Qed.

Inductive Nat : Type :=
| Z : Nat
| Suc : Nat -> Nat.

Definition Eq_Nat (N1 N2 : Nat) := N1 = N2.

Lemma Eq_Nat_equiv : Equivalence Eq_Nat.
Proof.
apply Build_Equivalence; unfold Eq_Nat in |- *.
auto.
apply Build_Partial_equivalence.
unfold Transitive in |- *; intros x y z H1 H2; apply (trans_eq H1 H2).
unfold Symmetric in |- *; intros x y H1; apply (sym_eq H1).
Qed.

Definition Set_of_nat : Setoid := Eq_Nat_equiv.

Structure > PSetoid : Type :=
{PCarrier :> Type;
Coherence : Relation PCarrier;
Prf_PER :> Partial_equivalence Coherence}.

Definition Total (A : PSetoid) (x : A) := Coherence x x.