PreCategory. refine (@Build_PreCategory (C * D) (fun s d => morphism C (fst s) (fst d) * morphism D (snd s) (snd d)) (fun x => (identity (fst x), identity (snd x))) (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) _ _ _ _); abstract ( repeat (simpl || intros [] || intro); try f_ap; auto with morphism ). Defined.
Require Import Basics.Tactics. Require Import Category.Strict. Require Import Types.Prod.