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

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

Definition

< integral Z-algebra

A

Heyting cancellation \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 cancellative identity
    d λ: (a:A)(a#0)× (b:A) (c:A)(ab=ac)(b=c)d_\lambda:\prod_{(a:A)} (a # 0) \times \prod_{(b:A)} \prod_{(c:A)} (a \cdot b = a \cdot c) \implies (b = c)
  • a right cancellative identity
    d λ: (a:A)(a#0)× (b:A) (c:A)(ba=ca)(b=c)d_\lambda:\prod_{(a:A)} (a # 0) \times \prod_{(b:A)} \prod_{(c:A)} (b \cdot a = c \cdot a) \implies (b = c)

Examples

See also

Revision on June 13, 2022 at 19:37:23 by Anonymous?. See the history of this page for a list of all contributions to it.