Homotopy Type Theory action > history (Rev #8)



Let (M,e,μ)(M, e, \mu) be a monoid and let XX be a set. An action is a function α f:M(XX)\alpha_f: M \to (X \to X) where there exist an identity term

i f:α f(e)=id Xi_f: \alpha_f(e) = id_X

and dependent function

c f: g:M h:Mα f(g)α f(h)=α f(μ(g,h))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.