s d (m : morphism C s d) : NaturalTransformation (Functor.Prod.Core.induced_snd F s) (Functor.Prod.Core.induced_snd F d). Proof. let F0 := match goal with |- NaturalTransformation ?F0 ?G0 => constr:(F0) end in let G0 := match goal with |- NaturalTransformation ?F0 ?G0 => constr:(G0) end in refine (Build_NaturalTransformation F0 G0 (fun d => @morphism_of _ _ F (_, _) (_, _) (m, @identity D d)) _). abstract t. Defined.
Require Import Category.Core Functor.Core Category.Prod Functor.Prod.Core NaturalTransformation.Core. Require Import Types.Prod.