Homotopy Type Theory biaction > history (Rev #4)

Idea

A ternary function which behaves as simultaneous actions on both the left and the right side:

 Definition

A single action monoid

Given a set $S$ and a monoid $(M, e, \mu)$, a $M$-biaction is a ternary function $\alpha:M \times S \times M \to S$ such that

• for all $s:S$, $\alpha(e, s, e) = s$

• for all $s:S$, $a:M$, $b:M$, $c:M$, and $d:M$, $\alpha(a, \alpha(b, s, c), d) = \alpha(\mu(a, b), s, \mu(c, d))$

Two action monoids

Given a set $S$ and monoids $(M, e_M, \mu_M)$ and $(N, e_N, \mu_N)$, a $M$-$N$-biaction is a ternary function $\alpha:M \times S \times N \to S$ such that

• for all $s:S$, $\alpha(e_M, s, e_N) = s$

• for all $s:S$, $a:M$, $b:M$, $c:N$, and $d:N$, $\alpha(a, \alpha(b, s, c), d) = \alpha(\mu_M(a, b), s, \mu_N(c, d))$

Left and right actions

The left $M$-action? is defined as

for all $a:M$ and $s:S$. It is a left action because

The right $N$-action? is defined as

for all $c:N$ and $s:S$. It is a right action because

The left $M$-action and right $N$-action satisfy the following identity:

• for all $s:S$, $a:M$ and $c:N$, $\alpha_M(a, \alpha_N(s, c)) = \alpha_N(\alpha_M(a, s), c)$.

This is because when expanded out, the identity becomes:

See also

• action

• bimodule

• biaction homomorphism?