(F G : Functor C D) (T : NaturalTransformation F G) (F' : Functor C' D') : NaturalTransformation (pointwise F F') (pointwise G F'). Proof. refine (Build_NaturalTransformation (pointwise F F') (pointwise G F') (fun f : object (D -> C') => (F' o f) oL T)%natural_transformation _). abstract t. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import FunctorCategory.Core NaturalTransformation.Paths Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import Functor.Pointwise.Core.