#Contents# * table of contents {:toc} ## Definition ## ### In sets ### Let $(M, e, \mu)$ be a [[monoid]] and let $X$ be a [[set]]. Then a __left action__ is a function $\alpha_l: M \times X \to X$ where there exist dependent identity terms $$x:X \vdash i_l(x): \alpha_l(e, x) = x$$ $$g:M, h:M, x:X \vdash c_l(g, h, x): \alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x)$$ and a __right action__ is a function $\alpha_r: X \times M \to X$ where there exist dependent identity terms $$x:X \vdash i_r(x): \alpha_r(x, e) = x$$ $$g:M, h:M, x:X \vdash c_r(g, h, x): \alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h))$$ A __curried action__ is a function $\alpha_f: M \to X \to X$ where there exist an identity term $$i_f: \alpha_f(e) = id_X$$ and dependent identity terms $$g:M, h:M \vdash c_f(g, h): \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))$$ ### In types ### There are a few generalisations of actions on sets to actions on types. #### H-actions #### Let $(M, e, \mu)$ be an [[A3-space]] and let $X$ be a [[type]]. Then a __left H-action__ is a function $\alpha_l: M \times X \to X$ where there exist dependent identity terms $$x:X \vdash i_l(x): \alpha_l(e, x) = x$$ $$g:M, h:M, x:X \vdash c_l(g, h, x): \alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x)$$ and a __right H-action__ is a function $\alpha_r: X \times M \to X$ where there exist dependent identity terms $$x:X \vdash i_r(x): \alpha_r(x, e) = x$$ $$g:M, h:M, x:X \vdash c_r(g, h, x): \alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h))$$ A __curried H-action__ is a function $\alpha_f: M \to X \to X$ where there exist an identity term $$i_f: \alpha_f(e) = id_X$$ and dependent identity terms $$g:M, h:M \vdash c_f(g, h): \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))$$ The identity types associated with an H-action are only required to hold up to homotopy. #### infinity-actions #### Let $(M, e, \mu)$ be an [[A-infinity-space]] and let $X$ be a [[type]]. Then a __left infinity-action__ is a function $\alpha_l: M \times X \to X$ where there exist dependent identity terms $$x:X \vdash i_l(x): \alpha_l(e, x) = x$$ $$g:M, h:M, x:X \vdash c_l(g, h, x): \alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x)$$ and associated coherence laws for higher homotopies, whatever they may be, and a __right infinity-action__ is a function $\alpha_r: X \times M \to X$ where there exist dependent identity terms $$x:X \vdash i_r(x): \alpha_r(x, e) = x$$ $$g:M, h:M, x:X \vdash c_r(g, h, x): \alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h))$$ and associated coherence laws for higher homotopies. A __curried infinity-action__ is a function $\alpha_f: M \to X \to X$ where there exist an identity term $$i_f: \alpha_f(e) = id_X$$ and dependent identity terms $$g:M, h:M \vdash c_f(g, h): \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))$$ and associated coherence laws for higher homotopies. The identity types associated with an infinity-action are required to hold up to coherent higher homotopy. #### pre-actions #### Let $(M, e, \mu)$ be a [[monoid]] and let $X$ be a [[type]]. Then a __left pre-action__ is a function $\alpha_l: M \times X \to X$ where there exist dependent identity terms $$x:X \vdash \iota_l(x): isContr(\alpha_l(e, x) = x)$$ $$g:M, h:M, x:X \vdash \kappa_l(g, h, x): isContr(\alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x))$$ and a __right pre-action__ is a function $\alpha_r: X \times M \to X$ where there exist dependent identity terms $$x:X \vdash \iota_r(x): isContr(\alpha_r(x, e) = x)$$ $$g:M, h:M, x:X \vdash \kappa_r(g, h, x): isContr(\alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h)))$$ The identity types associated with a pre-action are thus required to be contractible. ## See also ## * [[Higher algebra]] * [[monoid]] * [[H-space]]