# Homotopy Type Theory discrete integral domain > history (Rev #2)

## Definition

A discrete integral domain is a commutative discrete cancellation ring $(A, +, -, 0, \cdot, 1)$ with a term $p: (0 = 1) \to \emptyset$.