Monoidal.idr

The catgory of endofunctors is monoidal with regards to functor composition, that is, there is a bifunctor $\text{EndoCat}\times \text{EndoCat}\to \text{EndoCat}$ where the map on objects if given by the composition of the two endofunctors given in arguments, and the map on morphisms is given by the whiskering of natural transformations in $EndoCat$. This bifunctor in turns is associative and respects the identity laws needed to ensure $EndoCat$ is monoidal.

Proposition

Given a category $\mathcal{C}$ and the category $\mathcal{E}$ of endofunctors on $\mathcal{C}$, there is a bifunctor $({;}_{\mathcal{E}}):\mathcal{E}\times \mathcal{E}\to \mathcal{E}$ that composes endofunctors.

  monMultCompose :
    Bifunctor (EndoCat c) (EndoCat c) (EndoCat c)
  monMultCompose = MkFunctor
      { mapObj = (uncurry (⨾⨾))
      , mapHom = (\m1, m2, m3 => m3.π1 -⨾- m3.π2)
      , presId = presIdComp
      , presComp = presCompComp
      }

Using this bifunctor, we prove that the category of endofunctors is monoidal.

Proposition

Given a category $\mathcal{C}$ and the category $\mathcal{E}$ of endofunctors over $\mathcal{C}$, then $\mathcal{E}$ is monoidal wrt ${;}_{\mathcal{E}}$.

  EndoMonoidal : Monoidal (FunctorCat c c)
  EndoMonoidal = MkMonoidal
    { mult = monMultCompose
    , i = idF c
    , alpha = alpha
    , leftUnitor = leftUnitor
    , rightUnitor = rightUnitor
    }