C C' CF D D' DF (F : Functor C D) (G : Functor D C) (A : F -| G) (F' : Functor C' D') (G' : Functor D' C') (A' : F' -| G') (T : NaturalTransformation (F' o CF) (DF o F)) : NaturalTransformation (CF o G) (G' o DF) := (@left_morphism_of _ _ DF^op _ _ CF^op F^op G^op A^op F'^op G'^op A'^op T^op)^op.
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.