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 ________).