NaturalTransformation F' F. Proof. refine (_ o (@left_morphism_of C C 1 D D 1 G F A G' F' A' (_ o T o _)) o _)%natural_transformation; nt_solve_associator. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Identity Functor.Composition.Core. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import Functor.Dual NaturalTransformation.Dual. Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.Dual.