Homotopy Type Theory Z-algebra > history (Rev #3)

Definition

A $\mathbb{Z}$-algebra is an abelian group $(A, +, -, 0)$ with

• a binary operation $(-)\cdot(-): A \times A \to A$
• a left distributive identity
  $$d_\lambda:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} a \cdot (b + c) = a \cdot b + a \cdot c$$
• a right distributive identity
  $$d_\rho:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} (a + b) \cdot c = a \cdot c + b \cdot c$$

Examples

• Every contractible type is a $\mathbb{Z}$-algebra.

• The integers are a $\mathbb{Z}$-algebra.

• The rational numbers are a $\mathbb{Z}$-algebra.

See also

• abelian group

• unital Z-algebra

• cancellation Z-algebra

• division Z-algebra