Action.idr

Categorical action

The term action first appeared in the context of group actions which have the form $\oslash :C\times D\to D$ where $D$ is a group and $C$ is a set. We say that $C$ is acting on $D$ or that $\oslash$ is an action of $C$ on $D$.

We can generalise this notion for any category $D$ with a monoidal category $C$ using a bifunctor $\oslash :C\otimes D\to D$ and some coherence conditions.

Definition

Given two categories $\mathcal{C}$ and $\mathcal{D}$, with $\mathcal{C}$ being monoidal $(\otimes ,I,\alpha ,l,r)$ we say that $\mathcal{C}$ acts on $\mathcal{D}$ if we the following:

• A bifunctor called the action $\oslash :\mathcal{C}\times \mathcal{D}\to \mathcal{D}$
• A natural isomorphism called the “actor” $a:\forall x,y\in |\mathcal{C}|,z\in |\mathcal{D}|.(x\otimes y)\oslash z\iff x\oslash (y\oslash z)$
• A natural transformation neutralising the monoidal unit $e:I\oslash x\iff x$
• There is a commutative pentagon relating $(((x\otimes y)\otimes z)\oslash w)$ and $x\oslash (y\oslash (z\oslash w))$ given by $\alpha \times i{d}_w;a;i{d}_x\times a=a;a$
• There is a left unitor: $a;l\oslash id=e$
• There is a right unitor: $a;id\oslash e=r\oslash id$

public export
record Action
  {0 o1, o2 : Type} (c : Category o1) (d : Category o2)
  (mon : Monoidal c) where
  constructor MkAction
  action : Bifunctor c d d

Equipped with our action we define the actor diagram that ensures the relationship between the monoidal structure of $\mathcal{C}$ and the bifunctor. It’s a little bit hard to follow what f1 and f2 are but they are each branch of the diagram in figure \ref{fig:actor-diag}

  actor : let 0 f1 : (c × (c × d)) ->> d
              f1 = pair (idF c) action ⨾⨾ action
              0 f2 : (c × (c × d)) ->> d
              f2 = assocR ⨾⨾ pair mon.mult (idF d) ⨾⨾ action
           in f1 =~= f2

And our unitor diagram ensuring the relationship between the action and the monoidal unit of $\mathcal{C}$

  unitor : idF d =~= Bifunctor.applyL {a = c} mon.i action

This previous definition makes use of natural isomorphisms, but we can also define a notion of lax action that makes use of natural transformations instead, ensuring the conversion only goes one way.

Definition

A lax action is an action using natural transformation instead of natural isomorphisms.

We give a matching idris definition. It is this definition of action that we are going to use for Containers.

record LaxAction {0 o1, o2 : Type}
  (c : Category o1) (d : Category o2)
  (mon : Monoidal c) where
  constructor MkLaxAction
  laction : Bifunctor c d d
  lactor : let 0 f1, f2 : (c × (c × d)) ->> d
               f1 = pair (idF c) laction ⨾⨾ laction
               f2 = assocR ⨾⨾ pair mon.mult (idF d) ⨾⨾ laction
            in f1 =>> f2
  lunitor : idF d =>> Bifunctor.applyL {a = c} mon.i laction

From an action we can obtain a lax-action by only projecting the natural transformations out of the natural isomorphisms.

Proposition

From any action $(\oslash ,m,u)$, we can derive a lax-action by projecting out one side of the natural isomorphisms $m$ and $u$.

relax : {0 o1, o2 : Type} -> {c : Category o1} -> {d : Category o2} ->
        {0 mon : Monoidal c} ->
        Action c d mon -> LaxAction c d mon
relax act = MkLaxAction
    { laction = act.action
    , lactor = act.actor.nat
    , lunitor = act.unitor.nat
    }

A Monoidal Category is a Self-Action

A monoidal category is a special case of an action where the acting category is the same as the category being acted upon. We formalise this idea by introducing monoidal categories as a self-action and derive an action $\oslash :\mathcal{D}\times \mathcal{D}\to \mathcal{D}$ by simply reusing the monoidal product.

Proposition

From any monoidal category $\mathcal{C}$ emerges an action of $\mathcal{C}$ on itself.

monoidalSelfAction : {0 cat : Category _} ->
    (mon : Monoidal cat) -> Action cat cat mon
monoidalSelfAction mon = MkAction
  { action = mon.mult
  , actor = mon.alpha
  , unitor = symNT (mon.leftUnitor)
  }