# Homotopy Type Theory action > history (changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

# 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))$