MonadAction.idr

Monads From Actions

After studying both monads and actions, we can build the next result: how to produce monadsa given a categorical action.

Theorem

Given a monoidal category $\mathcal{C}$ $(\otimes ,I,\alpha ,l,r)$, a monoid $m\in \mathcal{C}$, and an action $(\oslash :\mathcal{C}\times \mathcal{D}\to \mathcal{D},act,i)$ of this monoidal category on $\mathcal{D}$, then the partially applied functor $m\oslash \_:\mathcal{D}\to \mathcal{D}$ is a monad.

To produce a monad we need to give its functor and its two natural transformations. For this, we first make precise what we have available before we define the functor. We will need:

• A category $\mathcal{D}$
• A monoidal category $\mathcal{C}$ with $(\otimes :C\times C\to C,I\in C)$
• A monoid $m\in \mathcal{C}$
• A monoidal action $(\oslash :\mathcal{C}\times \mathcal{D}\to \mathcal{D},act:x\oslash (y\oslash z)->(x\otimes y)\oslash z,e:x->I\oslash x)$

Using the above, we can define a functor $T:\mathcal{D}\to \mathcal{D}$ by partially applying our action to our monoid $m$, in other words, $T(x)=m\oslash x$.

This allows us to write explicitly what the natural tranformations of a suitable monad should be. The monadic unit $\eta :Id(x)\Rightarrow T(x)$ can be written as $Id(x)\Rightarrow m\oslash x$ is given by the lax unitor $e$. Similarly, the monadic multiplication $\mu :T(T(x))\Rightarrow T(x)$ can be written as $(m\oslash (m\oslash x))\Rightarrow (m\oslash x)$ and is given by composing the actor of the action with the monoidal multiplication $act;(\otimes \times id)$.

• [!] finish the diagrams programmatically

We implement monads from action in Idris by first parameterising all the data we need.

parameters
  (0 o1, o2: Type)
  (cat1 : Category o1)
  (cat2 : Category o2)
  (mon : Monoidal cat1)
  (act : LaxAction cat1 cat2 mon)
  (m : MonoidObject {o=o1} {cat=cat1} {mon})

Then we define the functor that we claim is a monad, that is $T(x)=m\oslash x$.

  T : Endo cat2
  T = applyL m.obj act.laction

we define the unit of the monad a $Id\Rightarrow F$ by composing vertically the unitor from the action $x\Rightarrow I\oslash x$ with the map $I\oslash x\Rightarrow m\oslash x$ emerging from the neutral map of the monoid $e:I\to m$

  unit : idF cat2 =>> T
  unit = act.lunitor ⨾⨾⨾ applyNT m.η act.laction

The multiplication is a map $T;T\Rightarrow T$ which expands to $m\oslash (m\oslash x)\Rightarrow m\oslash x$. Its codomain almost matches the actor map $x\oslash (y\oslash z)\Rightarrow (x\otimes y)\oslash z$ and the monoid operation on $m$ $(\ast ):m\otimes m\to m$ compose

We define an alias for the functor $F^{\prime }(x)=(m\otimes m)\oslash x$

  -- the functor F'(x) = (m ⊗ m) ⊘ x
  F' : Endo cat2
  F' = applyL {a = cat1} ((m.obj ⊗ m.obj)) act.laction

And we use it to define the natural transformation $(m\otimes m)\oslash x\Rightarrow m\oslash x$ via the multiplication of the monoid object.

  multAction : F' =>> T
  multAction = applyNT m.mult act.laction

We need to partially apply the actor map to be a natural transformation $m\oslash (m\oslash x)\Rightarrow (m\otimes m)\oslash x)$, we can do it by applying $M$ using whiskering but in this case it was faster to write down the map manually.

  (⊘) : o1 -> o2 -> o2
  (⊘) x y = act.laction.mapObj (x && y)
  private infixr 3 ⊘
 
  (~⊘~) : {x, y : o1} -> {z, w : o2} -> (x ~> y) {cat=cat1} -> z ~> w -> x ⊘ z ~> y ⊘ w
  (~⊘~) m1 m2 = act.laction.mapHom (x && z) (y && w) (m1 && m2)
  private infixr 3 ~⊘~
 
  actor : (x, y : o1) -> (z : o2) -> x ⊘ (y ⊘ z) ~> (x ⊗ y) ⊘ z
  actor x y z = act.lactor.component (x && (y && z))
 
  unitor : (x : o2) -> x ~> mon.i ⊘ x
  unitor x = act.lunitor.component x
 
  private infixr 3 ⊘>
 
  -- This could be done with careful composition of act.lactor and some lemmas about apply
  -- but writing out the definition is actually easier
  appActor : T ⨾⨾ T =>> F'
  appActor = MkNT
    (\v => actor m.obj m.obj v)
    (\x, y, h => let
      0 steps : CongPipeline ? ?
      steps =
         Cong (\vx =>
            (actor m.obj m.obj x) |>
            (vx ~⊘~ h))
              [ cat1.id (m.obj ⊗ m.obj)
              , cat1.id m.obj -⊗- cat1.id m.obj]
         >| ((cat1.id m.obj ~⊘~ (cat1.id m.obj ~⊘~ h)) |>
            (actor m.obj m.obj y))
         :: Nil
      in runProof steps
        [ sym (mon.mult.presId (m.obj && m.obj))
        , act.lactor.commutes
            (m.obj && (m.obj && x))
            (m.obj && (m.obj && y))
            (cat1.id m.obj && (cat1.id m.obj && h))
        ]
    )

Using the applied actor map and the action we obtain the multiplication morphism of our monad

  mult : T ⨾⨾ T =>> T
  mult = appActor ⨾⨾⨾ multAction

Those definitions bring us to the definition of $m\oslash \_$ as a monad in $\mathcal{D}$, the coherence diagrams are left in appendix.

• complete squares

• finish the coherence diagrams in idris

  MonadFromLaxAction : Monad cat2 T
  MonadFromLaxAction = MkMonad unit mult square identityLeft identityRight