- comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (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;
- id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
+ 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