Homotopy Type Theory Heyting skewfield > history (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

Definition

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

Examples

• The rational numbers are a Heyting skewfield.

• Every discrete skewfield is a Heyting skewfield.

• Every Heyting field is a Heyting skewfield.

See also

• ring

• skewfield