+definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
+definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
+definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
+
+record equivalence_relation1 (A:Type) : Type ≝
+ { eq_rel1:2> A → A → CProp;
+ refl1: reflexive1 ? eq_rel1;
+ sym1: symmetric1 ? eq_rel1;
+ trans1: transitive1 ? eq_rel1
+ }.
+
+record setoid1: Type ≝
+ { carr1:> Type;
+ eq1: equivalence_relation1 carr1
+ }.
+
+definition setoid1_of_setoid: setoid → setoid1.
+ intro;
+ constructor 1;
+ [ apply (carr s)
+ | constructor 1;
+ [ apply (eq_rel s);
+ apply (eq s)
+ | apply (refl s)
+ | apply (sym s)
+ | apply (trans s)]]
+qed.
+
+coercion setoid1_of_setoid.
+
+(*
+definition Leibniz: Type → setoid.
+ intro;
+ constructor 1;
+ [ apply T
+ | constructor 1;
+ [ apply (λx,y:T.cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y)
+ | alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
+ apply refl_eq
+ | alias id "sym_eq" = "cic:/matita/logic/equality/sym_eq.con".
+ apply sym_eq
+ | alias id "trans_eq" = "cic:/matita/logic/equality/trans_eq.con".
+ apply trans_eq ]]
+qed.
+
+coercion Leibniz.
+*)
+
+interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).