Action.idr

We’ve shown how to build monads from actions, we’re going to use that fact now to build monads from the ▶ action. This operation forms an action $\mathcal{C}on{t}^{\#}\times \mathcal{C}ont\to \mathcal{C}ont$ which we prove in this module. We refer to the definition of Action from section$\text{ref}def:action$.

• add hte missing coherence diagrams

Proposition

$▶$ is an action of $\mathcal{C}on{t}^{\#}$ on $\mathcal{C}ont$

public export
ForallLaxAction : LaxAction ContCart Cont Cart.SequenceMonoidal
ForallLaxAction = MkLaxAction
    { laction = ForallSeqBifunctor
    , lactor = ?actorType
    , lunitor = ?unitorType
    }