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

Definition

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

• a term $1: A$
• a left unit identity for $\cdot$
  $$u_\lambda:\prod_{(a:G)} 1 \cdot a = a$$
• a right unit identity for $\cdot$
  $$u_\rho:\prod_{(a:G)} a \cdot 1 = a$$

Properties

A unital $\mathbb{Z}$-algebra is an H-space in abelian groups.

Examples

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

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

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

See also

• H-space

• Z-algebra

• ring