X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fcategories.ma;h=6d57deddb02d493a2e6c3b8a0d178a5ce01cac14;hb=bf7be462a06e739b39af20f72362857e849a2aa0;hp=310aa709e2e0f1fe8ec1e325542bc23d3873e4c8;hpb=a580ff5c627c4148cdd3649ead20f4fac0f78be8;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma
index 310aa709e..6d57deddb 100644
--- 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,17 +19,13 @@ 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;
    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
  }.
 
-notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
-interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
-interpretation "arrows" 'arrows A B = (unary_morphism A B).
-
 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
 
@@ -27,8 +37,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 ≔ ;
@@ -55,7 +65,7 @@ ndefinition TYPE : setoid1.
 @ setoid; @; 
 ##[ #T1; #T2; 
     alias symbol "eq" = "setoid eq".
-    napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
+    napply (∃f:T1 ⇒_0 T2.∃g:T2 ⇒_0 T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption; 
 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg'; 
@@ -73,7 +83,7 @@ unification hint 0 ≔ ;
    
 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
  { fun01:1> A → B;
-   prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
+   prop01: ∀a,a'. eq0 ? a a' → eq1 ? (fun01 a) (fun01 a')
  }.
  
 interpretation "prop01" 'prop1 c  = (prop01 ????? c).