Homotopy Type Theory monoid > history (Rev #2)

Definition

A monoid consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • A left unitor
    λ: (a:A)μ(e,a)=a\lambda:\prod_{(a:A)} \mu(e,a)=a
  • A right unitor
    ρ: (a:A)μ(a,e)=a\rho:\prod_{(a:A)} \mu(a,e)=a
  • An asssociator
    α: (a:A) (b:A) (c:A)μ(μ(a,b),c)=μ(a,μ(b,c))\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))
  • A 0-truncator
    τ 0: (a:A) (b:A) (c:a=b) (d:a=b) (x:c=d) (y:c=d)x=y\tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \prod_{(d:a=b)} \sum_{(x:c=d)} \prod_{(y:c=d)} x=y

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 February 4, 2022 at 05:31:27 by Anonymous?. See the history of this page for a list of all contributions to it.