Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / matita / nlibrary / sets / setoids2.ma

diff --git a/matitaB/matita/nlibrary/sets/setoids2.ma b/matitaB/matita/nlibrary/sets/setoids2.ma
index 34036a48b37becddc01b1538ab9d4e46e3d831e9..112b19b98a15e20db14b18fb9ad2ee4084121c76 100644 (file)
--- 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')
  }.