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.