include "properties/relations2.ma".
include "sets/setoids1.ma".
-nrecord setoid2: Type[3] ≝
+record setoid2: Type[3] ≝
{ carr2:> Type[2];
eq2: equivalence_relation2 carr2
}.
-ndefinition setoid2_of_setoid1: setoid1 → setoid2.
- #s; @ (carr1 s); @ (carr1 s) (eq1 ?)
- [ napply refl1
- | napply sym1
- | napply trans1]
-nqed.
+definition setoid2_of_setoid1: setoid1 → setoid2.
+ #s @(mk_setoid2 … (carr1 s))
+ @(mk_equivalence_relation2 … (carr1 s) (eq1 ?))
+ /2/
+qed.
(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
on _s: setoid to setoid1.*)
interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y).
interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
-interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
(*
notation > "hvbox(a break =_12 b)" non associative with precedence 45
interpretation "trans1" 'trans r = (trans1 ????? r).
interpretation "trans" 'trans r = (trans ????? r).
-nrecord unary_morphism2 (A,B: setoid2) : Type[2] ≝
+record unary_morphism2 (A,B: setoid2) : Type[2] ≝
{ fun12:1> A → B;
prop12: ∀a,a'. eq2 ? a a' → eq2 ? (fun12 a) (fun12 a')
}.
-nrecord binary_morphism2 (A,B,C:setoid2) : Type[2] ≝
+record binary_morphism2 (A,B,C:setoid2) : Type[2] ≝
{ fun22:2> A → B → C;
prop22: ∀a,a',b,b'. eq2 ? a a' → eq2 ? b b' → eq2 ? (fun22 a b) (fun22 a' b')
}.