X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdatatypes%2Fcategories.ma;h=692f977df86914ff844e15c9594930b21e7994d0;hb=04c05cf08605156ba8c6fa7225b4a90496c03698;hp=e90e1457d222d23702ec37792f252ac67a270b6a;hpb=da03907a38982b8b45459213f2b9581accac5143;p=helm.git

diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma
index e90e1457d..692f977df 100644
--- a/helm/software/matita/library/datatypes/categories.ma
+++ b/helm/software/matita/library/datatypes/categories.ma
@@ -192,14 +192,14 @@ record category1 : Type ≝
    comp1: ∀o1,o2,o3. binary_morphism1 (arrows1 o1 o2) (arrows1 o2 o3) (arrows1 o1 o3);
    comp_assoc1: ∀o1,o2,o3,o4. ∀a12,a23,a34.
     comp1 o1 o3 o4 (comp1 o1 o2 o3 a12 a23) a34 = comp1 o1 o2 o4 a12 (comp1 o2 o3 o4 a23 a34);
-   id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a;
-   id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a
+   id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a;
+   id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a
  }.
 
 notation "'ASSOC'" with precedence 90 for @{'assoc}.
 notation "'ASSOC1'" with precedence 90 for @{'assoc1}.
 
-interpretation "category1 composition" 'compose x y = (fun1 ___ (comp1 ____) x y).
+interpretation "category1 composition" 'compose x y = (fun1 ___ (comp1 ____) y x).
 interpretation "category1 assoc" 'assoc1 = (comp_assoc1 ________).
-interpretation "category composition" 'compose x y = (fun ___ (comp ____) x y).
+interpretation "category composition" 'compose x y = (fun ___ (comp ____) y x).
 interpretation "category assoc" 'assoc = (comp_assoc ________).