# Homotopy Type Theory discrete integral domain > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## Definition

A

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