Applying natural transformation on left and right?

[formrre]

I have

T T' : Functor B A,
φ : NaturalTransformation S' S,
ψ : NaturalTransformation T T',
(a : Adjoint S T),
(a' : Adjoint S' T')

I am trying to construct NaturalTransformation (Adjoint.Hom[L-,-] a) (Adjoint.Hom[L-,-] a') by left applying φ and also similar transformation with Hom[-,R-], by right applying ψ. Which functions should I use? For context this is trying to define the adjointness of morphisms (1.9) from ADJOINT FUNCTORS AND TRIPLES by Eilenberg and Moore.

[ncfavier]

Some pieces of the puzzle I'd expect you to have to use: _⁂ⁿ_, _∘ˡ_, φ.op.

[formrre]

Here are my concrete solutions based on @ncfavier 's suggestion, which could probably be generalized and type signatures written somewhat nicer:

lapplyNT :
   {o l e o' l' e' : _}
   {A : Category o l e} {B : Category o' l' e'}
   {S S' : Functor A B}
   (φ : NaturalTransformation S' S)
   -> NaturalTransformation
     (Hom.Hom[-,-] B ∘F (Functor.op S  ⁂ idF))
     (Hom.Hom[-,-] B ∘F (Functor.op S' ⁂ idF))
lapplyNT φ = Hom.Hom[-,-] _ ∘ˡ ((NaturalTransformation.op φ) ⁂ⁿ idNT)

rapplyNT :
   {o l e o' l' e' : _}
   {A : Category o l e} {B : Category o' l' e'}
   {T T' : Functor B A}
   (φ : NaturalTransformation T T')
   ->  NaturalTransformation
      (Hom.Hom[-,-] A ∘F (idF ⁂ T ))
      (Hom.Hom[-,-] A ∘F (idF ⁂ T'))
rapplyNT φ = Hom.Hom[-,-] _ ∘ˡ ( idNT ⁂ⁿ φ )

[JacquesCarette]

Thanks for using the Discussion forum for this. Glad it worked for you.