NaturalTransformation (F' o CF) (DF o F). Proof. refine ((_) o (counit A' oR (DF o F)) o _ o (F' oL ((T oR F) o _ o (CF oL unit A) 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.