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

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

Definition

A Heyting field is a commutative Heyting ~~skewfield~~ reciprocal 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 rational numbers are a Heyting field.
Every discrete field is a Heyting field.

See also

Revision on March 14, 2022 at 23:52:51 by Anonymous?. See the history of this page for a list of all contributions to it.