Homotopy Type Theory Heyting division ring > history (Rev #2, changes)

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

Definition

< division ring

A

Heyting division 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))
  • a left divisibility identity
    d λ: (a:A)((a#0)× (c:A) (b:A)ab=c)d_\lambda:\prod_{(a:A)} \left( (a # 0) \times \prod_{(c:A)} \left\Vert \sum_{(b:A)} a \cdot b = c \right\Vert \right)
  • a right divisibility identity
    d λ: (a:A)((a#0)× (c:A) (b:A)ba=c)d_\lambda:\prod_{(a:A)} \left( (a # 0) \times \prod_{(c:A)} \left\Vert \sum_{(b:A)} b \cdot a = c \right\Vert \right)

Properties

Every Heyting division ring is a Heyting reciprocal ring.

Examples

See also

Revision on June 12, 2022 at 20:34:02 by Anonymous?. See the history of this page for a list of all contributions to it.