Homotopy Type Theory biaction > history (Rev #1)

Idea

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

 Definition

Given a set $S$ and monoids $(M, e_M, \mu_M)$ and $(N, e_N, \mu_N)$, a two-sided action 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))$

The left action is defined as

for $a:M$ and $s:S$, and the right action is defined as

for $c:N$ and $s:S$.

See also

• Malcev operation?

• action

• bimodule