Homotopy Type Theory discrete domain > history (Rev #1)

Definition

A discrete domain is a discrete cancellation ring $(A, +, -, 0, \cdot, 1, #)$ with a term $p: 0 # 1$.

Examples

• The integers are a discrete domain.

• The rational numbers are a discrete domain

• Every discrete skewfield is a discrete skewfield.

See also

• ring

• domain