#
Homotopy Type Theory
action > history (Rev #8)

# Contents

## Definition

Let $(M, e, \mu)$ be a monoid and let $X$ be a set. An **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 function

$c_f: \prod_{g:M} \prod_{h:M} \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))$

## See also

Revision on June 13, 2022 at 22:33:04 by
Anonymous?.
See the history of this page for a list of all contributions to it.