1) as usual, I took the reverse notation for composition.

[helm.git] / helm / software / matita / library / datatypes / categories.ma

diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma
index e90e1457d222d23702ec37792f252ac67a270b6a..692f977df86914ff844e15c9594930b21e7994d0 100644 (file)
--- 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 ________).