Homotopy Type Theory Heyting field > history (Rev #3)

Definition

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

Examples

• The rational numbers are a Heyting field.

• Every discrete field is a Heyting field.

See also

• ring

• field

• ordered field