Homotopy Type Theory
Heyting division Z-algebra > history (changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Definition
< division algebra
A
Heyting division $\mathbb{Z}$-algebra is a $\mathbb{Z}$-algebra $(A, +, -, 0, \cdot)$ 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
See also
Last revised on June 12, 2022 at 20:12:52.
See the history of this page for a list of all contributions to it.