Homotopy Type Theory commutative monoid > history (changes)

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


< commutative monoid


commutative monoid consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • A contractible left unit identity
    c λ: (a:G)isContr(μ(e,a)=a)c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)
  • A contractible right unit identity
    c ρ: (a:G)isContr(μ(a,e)=a)c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)
  • A contractible associative identity
    c α: (a:G) (b:G) (c:G)isContr(μ(μ(a,b),c)=μ(a,μ(b,c)))c_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))
  • A contractible commutative identity
    c κ: (a:A) (b:A)isContr(μ(a,b)=μ(b,a))c_\kappa:\prod_{(a:A)} \prod_{(b:A)} isContr(\mu(a, b)=\mu(b, a))
  • A 0-truncator
    τ 0: (a:A) (b:A)isProp(a=b)\tau_0: \prod_{(a:A)} \prod_{(b:A)} isProp(a=b)


  • The integers are a commutative monoid.

See also

Last revised on June 14, 2022 at 16:33:58. See the history of this page for a list of all contributions to it.