Homotopy Type Theory ring > history (Rev #6)

Definition

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

• an associative identity for $\cdot$
  $$m_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} (a\cdot b)\cdot c = a\cdot (b\cdot c)$$

Properties

A ring is an A3-space in abelian groups.

Examples

• Every contractible type is a ring.

• The integers are a ring.

• The rational numbers are a ring.

See also

• A3-space

• unital Z-algebra

• commutative ring

• cancellation ring

• power function

• polynomial function