Homotopy Type Theory Heyting reciprocal ring > history (changes)

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

Definition

< reciprocal ring

A

Heyting reciprocal ring is a ring (A,+,,0,,1)(A, +, -, 0, \cdot, 1) with

  • a tight apartness relation type family a#ba # b for a:Aa:A, b:Ab:A
  • a term showing that all endofunctions of AA are strongly extensional
    s: (f:AA) (a:A) (b:A)(a#b)(f(a)#f(b))s:\prod_{(f:A \to A)} \prod_{(a:A)} \prod_{(b:A)} (a # b) \to (f(a) # f(b))
  • an identity showing that every term apart from 00 has a reciprocal (a two-sided multiplicative inverse)
    r: (a:A)((a#0)× (b:A)(ab=1)×(ba=1))r:\prod_{(a:A)} \left( (a # 0) \times \left\Vert \sum_{(b:A)} (a \cdot b = 1) \times (b \cdot a = 1) \right\Vert \right)

Properties

Every Heyting reciprocal ring is a Heyting division ring.

Examples

See also

Last revised on June 12, 2022 at 20:37:00. See the history of this page for a list of all contributions to it.