C C' D F G F' G' (T : @NaturalTransformation C D F G) (T' : @NaturalTransformation C' D F' G') : NaturalTransformation (F + F') (G + G'). Proof. refine (Build_NaturalTransformation (F + F') (G + G') (fun x => match x with | Basics.Overture.inl c => T c | Basics.Overture.inr c' => T' c' end) _). abstract ( repeat (intros [] || intro); simpl; auto with natural_transformation ). Defined.
Require Import Category.Sum Functor.Sum NaturalTransformation.Core.