fact: Definition Build_PreCategory object morphism identity compose associativity left_identity right_identity := @Build_PreCategory' object morphism identity compose associativity (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _)) left_identity right_identity (fun _ => left_identity _ _ _).
imports: Overture Basics.Notations