Showing changes from revision #12 to #13: Added | Removed | Changed

Contents

Definition

A monoid consists is of aset $M$ with an element $e:M$ and a function $\alpha:M \to (M \to M)$ such that

• A type$A$

  $\alpha(1) = \mathrm{id}_M$

  ,
• A basepoint$e:A$

  for all $a:M$, $\alpha(a)(1) = a$

• A binary operation$\mu : A \to A \to A$

  for all $a:M$, $b:M$, and $c:M$, $(\alpha(a) \circ \alpha(b))(c) = \alpha(a)(\alpha(b)(c))$

• A contractible left unit identity
  $$c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)$$
• A contractible right unit identity
  $$c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)$$
• A contractible associative identity
  $$c_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))$$
• A 0-truncator
  $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} isProp(a=b)$$