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

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

Definition

A discrete domain is a discrete cancellation ring $(A,+,-,0,\cdot ,1,\#)$ (A, +, -, 0, \cdot, 1, 1) #) with a term $p:(0<span><del\; class="diffmod">\; \#</del><ins\; class="diffmod">\; =</ins></span>1)\to \varnothing$ p: 0 (0 # = 1 1) \to \emptyset.

Examples

• The integers are a discrete domain.

• The rational numbers are a discrete domain

• Every discrete skewfield is a discrete domain.

See also

• ring

• domain