(C D : PreCategory) : PreCategory. Proof. refine (@Build_PreCategory (C + D) (sum_morphism C D) (sum_identity C D) (sum_compose C D) _ _ _ _); abstract ( repeat (simpl || apply istrunc_S || intros [] || intro); auto with morphism; typeclasses eauto ). Defined.