Curryfication of binary setoids.

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 8ca0254b4387e4655c791043da7c9fce29c111ae..685d6248059afb3e162ae4ec00ea1304f05318af 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -16,7 +16,7 @@ include "sets/sets.ma".
 
 nrecord magma_type : Type[1] ≝
  { mtcarr:> setoid;
-   op: binary_morphism mtcarr mtcarr mtcarr
+   op: unary_morphism mtcarr (unary_morph_setoid mtcarr mtcarr)
  }.
 
 nrecord magma (A: magma_type) : Type[1] ≝

diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma
index 310aa709e2e0f1fe8ec1e325542bc23d3873e4c8..38c8129fa28d3d7dc0a55a5d51a588102f284d66 100644 (file)
--- a/helm/software/matita/nlibrary/sets/categories.ma
+++ b/helm/software/matita/nlibrary/sets/categories.ma
@@ -1,3 +1,17 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
 
@@ -5,7 +19,7 @@ nrecord category : Type[2] ≝
  { objs:> Type[1];
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism (arrows o2 o3) (arrows o1 o2) (arrows o1 o3);
+   comp: ∀o1,o2,o3. unary_morphism (arrows o2 o3) (unary_morph_setoid (arrows o1 o2) (arrows o1 o3));
    comp_assoc: ∀o1,o2,o3,o4. ∀a34,a23,a12.
     comp o1 o3 o4 a34 (comp o1 o2 o3 a23 a12) = comp o1 o2 o4 (comp o2 o3 o4 a34 a23) a12;
    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o2) a = a;
@@ -27,8 +41,8 @@ ndefinition SETOID : category.
 ##| napply unary_morph_setoid;
 ##| #o; @ (λx.x); #a; #b; #H; napply H;
 ##| napply comp_binary_morphisms; (*CSC: why not ∘?*)
-##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
-##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
+##| #o1; #o2; #o3; #o4; #f; #g; #h; #x; #x'; #Hx; nnormalize; napply (†(†(†Hx)))
+##|##6,7: #o1; #o2; #f; #x; #x'; #Hx; nnormalize; napply (†Hx) ]
 nqed.
 
 unification hint 0 ≔ ;

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 84d320e7f1f9763edf9ff4d3d55361cdab0fbebf..b92fe9ab3011d9bcbcb75637b51c886c43de6d05 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -128,9 +128,9 @@ nlemma partition_splits_card:
     nlapply (Hc y I); *; #index; *; #Hi1; #Hi2;
     nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2;
     nlapply (f_sur ???? (fi nindex) y ?)
-     [ alias symbol "refl" = "refl".
-alias symbol "prop1" = "prop11".
-alias symbol "prop2" = "prop21 mem".
+     [ alias symbol "refl" (instance 3) = "refl".
+alias symbol "prop2" (instance 2) = "prop21".
+alias symbol "prop1" (instance 4) = "prop11".
 napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
     *; #nindex2; *; #Hni21; #Hni22;
     nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index f9fcfd0202591711cb85951a89ba095b46a626bc..58fe2184456dc39dddfa35854563ac686c960b82 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -93,14 +93,11 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o
  (* -------------------------------------------------------------------- *) ⊢
                               fun1 ?? R ≡ (composition … f g).
 
-(*                              
 ndefinition comp_binary_morphisms:
  ∀o1,o2,o3.
-  binary_morphism (unary_morph_setoid o2 o3) (unary_morph_setoid o1 o2)
-   (unary_morph_setoid o1 o3).
-#o1; #o2; #o3; @
+  unary_morphism (unary_morph_setoid o2 o3)
+   (unary_morph_setoid (unary_morph_setoid o1 o2) (unary_morph_setoid o1 o3)).
+#o1; #o2; #o3; napply mk_binary_morphism
  [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*)
- | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
-   napply (.= †(eb x)); napply ea.
-nqed.
-*)
+ | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
+nqed.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index fa615c8e4d74600903d6e1cdd845eb3524ad6f3f..69e0958744de4f83c3257f88ad3b8e4ac78ef8fa 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -104,14 +104,11 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:unary_morphism1 o2 o3,g:unary_morphism
  (* -------------------------------------------------------------------- *) ⊢
                               fun11 ?? R ≡ (composition1 … f g).
                               
-(*
-ndefinition comp_binary_morphisms:
+ndefinition comp1_binary_morphisms:
  ∀o1,o2,o3.
-  binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2)
-   (unary_morphism1_setoid1 o1 o3).
-#o1; #o2; #o3; @
+  unary_morphism1 (unary_morphism1_setoid1 o2 o3)
+   (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)).
+#o1; #o2; #o3; napply mk_binary_morphism1
  [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
- | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
-   napply (.= †(eb x)); napply ea.
-nqed.
-*)
+ | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
+nqed.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index e7f9a5a15bed6ccbf0709169558c16a2497ff0dc..3e9214f37ce61fc5b9f18086aff74da37a8c91b1 100644 (file)
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -1,4 +1,16 @@
-
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "topology/igft.ma".
 

diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma
index 7235b4ba08bb164a12dc616f110aaaf8ad1a76c9..a4d833cae0007f8f7d78f3a888107357c1274292 100644 (file)
--- 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,10 +187,7 @@ 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]);                    
@@ -574,4 +566,4 @@ D*)
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
 
 D*)
-*)
\ No newline at end of file
+*)