Homotopy Type Theory Heyting division Z-algebra > history (Rev #2)


A Heyting division \mathbb{Z}-algebra is a $\mathbb{Z}$-algebra (A,+,,0,)(A, +, -, 0, \cdot) 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)


See also

Revision on February 28, 2022 at 19:14:08 by Anonymous?. See the history of this page for a list of all contributions to it.