X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids2.ma;h=112b19b98a15e20db14b18fb9ad2ee4084121c76;hb=71c124b4f171059ec3d29d5e53079000773ec851;hp=34036a48b37becddc01b1538ab9d4e46e3d831e9;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/nlibrary/sets/setoids2.ma b/matitaB/matita/nlibrary/sets/setoids2.ma
index 34036a48b..112b19b98 100644
--- a/matitaB/matita/nlibrary/sets/setoids2.ma
+++ b/matitaB/matita/nlibrary/sets/setoids2.ma
@@ -15,17 +15,16 @@
 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.*)
@@ -33,7 +32,7 @@ nqed.
 
 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
@@ -54,12 +53,12 @@ interpretation "trans2" 'trans r = (trans2 ????? r).
 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')
  }.