object morphism identity compose associativity left_identity right_identity := @' object morphism identity compose associativity (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _)) left_identity right_identity (fun _ => left_identity _ _ _).