update in groud_2 and models

[helm.git] / helm / software / matita / nlibrary / topology / igft-setoid.ma

diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma
index a4d833cae0007f8f7d78f3a888107357c1274292..276fa54805a117c729289f4b3e79e49869b1c9ae 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft-setoid.ma
+++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma
@@ -63,6 +63,7 @@ unification hint 0 ≔ A,B ;
            (* ----------------------------------- *) ⊢              
                   unary_morphism A B ≡ carr T. 
                 
+(*                
                 
 ndefinition TYPE : setoid1.
 @ setoid; @; 
@@ -111,7 +112,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.
@@ -140,6 +141,7 @@ 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;
@@ -566,4 +568,4 @@ D*)
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
 
 D*)
-*)
+*)*)
\ No newline at end of file