Homotopy Type Theory ring > history (Rev #11)

Definition

A ring is an abelian group $R$ with an element $1:R$ and a abelian group homomorphism $\alpha:R \to (R \times R)$ such that

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

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

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

We define the bilinear function $(-)\cdot(-):M \times M \to M$ as

Examples

• Every contractible type is a ring.

• The integers are a ring.

• The rational numbers are a ring.

See also

• abelian group

• monoid

• commutative ring