Monad.idr

Forall is a Monad

We’re going to use our monad-action theorem \thmref{thm:monad-action} to generate the witness that the Forall list is a monad in $\mathcal{C}ont$. For this we need a couple of crucial defintion, first we need the fact that $▶$ is a lax action, then we need a list monoid in $\mathcal{C}on{t}^{\#}$ with regards to the monoidal structure induced by $▶$. Finally

Proposition

$Forall$ is a monad via the $▶$ action.

public export
ForallMonadCont : Monad Cont ForallFunctor
ForallMonadCont = MonadFromLaxAction ? ?
    ContCart Cont SequenceMonoidal Action.ForallLaxAction Cartesian.ListMonoid

Forany is a Monad

Similarly, we’re going to use the fact that for each monoidal structure in a category $\mathcal{C}$ and a monoid $m\in \mathcal{C}$ the functor $m\otimes \_$ is a monad. To apply this to the Forany functor we need the monoidal structure induced by $⊳$ on $\mathcal{C}ont$ as well as the monoid object $ListCont$.

We then instanciate both those facts by reusing the monad-action theorem but mapping our monoidal category into a self-action

ListMonoidalAction : Action Cont Cont SequenceMonoidal
ListMonoidalAction = monoidalSelfAction SequenceMonoidal
 
ForanyMonadCont : Monad Cont ForanyFunctor
-- ForanyMonadCont = MonadFromLaxAction ? ?
--     Cont Cont SequenceMonoidal (relax ListMonoidalAction) Cont.ListMonoid