X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft-setoid.ma;h=a4d833cae0007f8f7d78f3a888107357c1274292;hb=d05dded8c907533b3aba2fcc75c82fa56478af0e;hp=30f2d161ee21296d76af768993e537e6c62b64ba;hpb=d5aca0dbfdc1770b3fa7e3c1338bfb7ffde8f89e;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma
index 30f2d161e..a4d833cae 100644
--- a/helm/software/matita/nlibrary/topology/igft-setoid.ma
+++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma
@@ -1,27 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
 
 include "sets/sets.ma".
 
-ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
-#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
-##[ #f; #g; napply (∀x,y. f x y = g x y);
-##| #f; #x; #y; napply #;
-##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
-##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
-nqed.
-
-ndefinition unary_morph_setoid : setoid → setoid → setoid.
-#S1; #S2; @ (unary_morphism S1 S2); @;
-##[ #f; #g; napply (∀x. f x = g x);
-##| #f; #x; napply #;
-##| #f; #g; #H; #x; napply ((H x)^-1);
-##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
-nqed.
-
 nrecord category : Type[2] ≝
  { objs:> Type[1];
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
+   comp: ∀o1,o2,o3. unary_morphism (arrows o1 o2) (unary_morph_setoid (arrows o2 o3) (arrows o1 o3));
    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
@@ -40,13 +37,11 @@ ndefinition SETOID : category.
 @; 
 ##[ napply setoid;
 ##| napply unary_morph_setoid;
-##| #o; @ (λx.x); #a; #b; #H; napply H;
-##| #o1; #o2; #o3; @; 
-    ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
-    ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
-        napply (.= (†(H1 x))); napply #; ##]
-##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
-##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
+##| #o; @ (λx.x); //
+##| #o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; @(λx.g (f x)) ]
+    nnormalize; /3/
+##| nnormalize; /4/
+##|##6,7: nnormalize; /2/ ]
 nqed.
 
 unification hint 0 ≔ ;
@@ -192,15 +187,12 @@ nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝
                 @ (f i); #a; #Ha; napply H1;
                 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]); 
                 
-                ##[##2: #E; alias symbol "refl" = "refl".
-                        alias symbol "prop2" = "prop21 mem".
-                        alias symbol "invert" = "setoid1 symmetry".
-                        napply (. (#‡E^-1)); napply Ha; ##]
+                ##[##2: #E; napply (. (#‡E^-1)); napply Ha; ##]
                         
                 @; #w; #Hw; nwhd;
                 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);                    
                   
-    
+(*    
   
 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
@@ -574,3 +566,4 @@ D*)
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
 
 D*)
+*)