(F : Functor C D) (F' G' : Functor C' D') (T' : NaturalTransformation F' G') : NaturalTransformation (pointwise F F') (pointwise F G'). Proof. refine (Build_NaturalTransformation (pointwise F F') (pointwise F G') (fun f : object (D -> C') => T' oR f oR F)%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.