## Definition ## A __Heyting division $\mathbb{Z}$-algebra__ is a [[Z-algebra|$\mathbb{Z}$-algebra]] $(A, +, -, 0, \times)$ with * 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. ## See also ## * [[Z-algebra]] * [[division Z-algebra]] * [[Heyting division ring]]