Homotopy Type Theory Heyting integral domain > history (Rev #3)

Definition

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

Examples

• The integers are a Heyting integral domain.

• The rational numbers are a Heyting integral domain

• Every discrete integral domain is a Heyting integral domain.

• Every Heyting field is a Heyting integral domain.

See also

• ring

• integral domain

• ordered integral domain