Homotopy Type Theory monoid > history (Rev #14)

Contents

Definition

A monoid is a set MM with an element e:Me:M and a function α:M(MM)\alpha:M \to (M \to M) such that

  • α(1)=id M\alpha(1) = \mathrm{id}_M

  • for all a:Ma:M, α(a)(1)=a\alpha(a)(1) = a

  • for all a:Ma:M, b:Mb:M, and c:Mc:M, (α(a)α(b))(c)=α(a)(α(b)(c))(\alpha(a) \circ \alpha(b))(c) = \alpha(a)(\alpha(b)(c))

We define the binary operation μ:M×MM\mu:M \times M \to M as

μ(a,b)α(a)(b)\mu(a, b) \coloneqq \alpha(a)(b)

Examples

  • The integers are a monoid.

  • Given a set AA, the type of endofunctions AAA \to A has the structure of an monoid, with basepoint id Aid_A, operation function composition.

See also

References

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