fact: Definition opposite (C : PreCategory) : PreCategory := @Build_PreCategory' C (fun s d => morphism C d s) (identity (C := C)) (fun _ _ _ m1 m2 => m2 o m1) (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _) (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _) (fun _ _ => @right_identity _ _ _) (fun _ _ => @left_identity _ _ _) (@identity_identity C) _.
imports: Category.Core Category.Objects