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

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

Definition

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