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

Definition

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

Examples

• The integers are a Heyting domain.

• The rational numbers are a Heyting domain

• Every discrete domain is a Heyting domain.

• Every Heyting skewfield is a Heyting skewfield.

See also

• ring

• domain