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

diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma
index 276fa5480..30f2d161e 100644
--- a/helm/software/matita/nlibrary/topology/igft-setoid.ma
+++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma
@@ -1,24 +1,27 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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. unary_morphism (arrows o1 o2) (unary_morph_setoid (arrows o2 o3) (arrows o1 o3));
+   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (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;
@@ -37,11 +40,13 @@ ndefinition SETOID : category.
 @; 
 ##[ napply setoid;
 ##| napply unary_morph_setoid;
-##| #o; @ (λx.x); //
-##| #o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; @(λx.g (f x)) ]
-    nnormalize; /3/
-##| nnormalize; /4/
-##|##6,7: nnormalize; /2/ ]
+##| #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 #; ##]
 nqed.
 
 unification hint 0 ≔ ;
@@ -63,7 +68,6 @@ unification hint 0 ≔ A,B ;
            (* ----------------------------------- *) ⊢              
                   unary_morphism A B ≡ carr T. 
                 
-(*                
                 
 ndefinition TYPE : setoid1.
 @ setoid; @; 
@@ -112,7 +116,7 @@ interpretation "d" 'd a i j = (nd ? a i j).
 interpretation "new I" 'I a = (nI ? a).
 
 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
-
+(*
 nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
 #A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
 nqed.
@@ -141,7 +145,6 @@ nlemma foo: ∀A:setoid.∀T:unary_morphism01 A TYPE.∀P:∀x:A.∀a:T x.CProp[
 ##[ @(f e);   
 *)
 
-(*
 ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
 #A; #a; #i; @ (image … i); #x; #y; #H; @;
 ##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
@@ -189,12 +192,15 @@ 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; napply (. (#‡E^-1)); napply Ha; ##]
+                ##[##2: #E; alias symbol "refl" = "refl".
+                        alias symbol "prop2" = "prop21 mem".
+                        alias symbol "invert" = "setoid1 symmetry".
+                        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 }.
@@ -568,4 +574,3 @@ D*)
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
 
 D*)
-*)*)
\ No newline at end of file