Homotopy Type Theory ring > history (Rev #8)

Definition

A ring is an abelian group $R$ with a term $1:R$, a bilinear function $(-)\cdot(-):R \times R \to R$, and a abelian group homomorphism $\alpha:R \to (R \times R)$ such that

• $\alpha(1) = \mathrm{id}_R$

• for all $a:R$ and $b:R$, $\alpha(a) \circ \alpha(b) = \alpha(a \cdot b)$

Examples

• Every contractible type is a ring.

• The integers are a ring.

• The rational numbers are a ring.

See also

• commutative ring

• power function

• polynomial function