Homotopy Type Theory Heyting division Z-algebra > history (Rev #3, changes)

• a tight apartness relation type family $a # b$ for $a:A$, $b:A$
• a term showing that all endofunctions of $A$ are strongly extensional
  $$s:\prod_{(f:A \to A)} \prod_{(a:A)} \prod_{(b:A)} (a # b) \to (f(a) # f(b))$$
• a left divisibility identity
  $$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_\lambda:\prod_{(a:A)} \left( (a # 0) \times \prod_{(c:A)} \left\Vert \sum_{(b:A)} b \cdot a = c \right\Vert \right)$$

Examples

• The rational numbers are a Heyting division $\mathbb{Z}$-algebra.

• Every discrete division Z-algebra is a Heyting division $\mathbb{Z}$-algebra.

• Every Heyting division ring is a Heyting division $\mathbb{Z}$-algebra.

See also

• Z-algebra

• division Z-algebra