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

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Definition

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

~~$m_\kappa:\prod_{(a:A)} \prod_{(b:A)} a\cdot b = b\cdot a$~~

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.

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

Definition

Examples

See also