#Contents# * table of contents {:toc} ## Idea ## The integers as familiar from school mathematics. ## Definitions ## The type of **integers**, denoted $\mathbb{Z}$, has several definitions as a [[higher inductive type]]. ### Definition 1 ### The integers are defined as the [[higher inductive type]] generated by: * A function $inj : \mathbf{2} \times \mathbb{N} \rightarrow \mathbb{Z}$. * An identity representing that positive and negative zero are equal: $\nu_0: inj(0, 0) = inj(1, 0)$. ### Definition 2 ### The integers are defined as the [[higher inductive type]] generated by: * A term $0 : \mathbb{Z}$. * A function $s : \mathbb{Z} \to \mathbb{Z}$. * A function $p_1 : \mathbb{Z} \to \mathbb{Z}$. * A function $p_2 : \mathbb{Z} \to \mathbb{Z}$. * A dependent product of identities representing that $p_1$ is a section of $s$: $$\sigma: \prod_{a:\mathbb{Z}} p_1(s(a)) = a$$ * A dependent product of identities representing that $p_2$ is a retracion of $s$: $$\rho: \prod_{a:\mathbb{Z}} s(p_2(a)) = a$$ ### Definition 3 ### The integers are defined as the [[higher inductive type]] generated by: * A term $0 : \mathbb{Z}$. * A function $s : \mathbb{Z} \to \mathbb{Z}$. * A function $p : \mathbb{Z} \to \mathbb{Z}$. * A dependent product of identities representing that $p$ is a section of $s$: $$\sigma: \prod_{a:\mathbb{Z}} p(s(a)) = a$$ * A dependent product of identities representing that $p$ is a retracion of $s$: $$\rho: \prod_{a:\mathbb{Z}} s(p(a)) = a$$ * A dependent product of identities representing the coherence condition: $$\kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)$$ ### Definition 4 ### The integers are defined as the [[higher inductive type]] generated by: * A term $0 : \mathbb{Z}$. * A function $s : \mathbb{Z} \to \mathbb{Z}$. * A function $n : \mathbb{Z} \to \mathbb{Z}$. * An identity representing that zero and negative zero are equal: $\nu: n(0) = 0$. * A dependent product of identities representing that negation is an involution: $$\iota: \prod_{a:\mathbb{Z}} n(n(a)) = a$$ * A dependent product of identities representing the coherence condition for the above: $$\kappa_\iota: \prod_{a:\mathbb{Z}} ap_n(\iota(a)) = \iota(a)$$ * A dependent product of identities representing that $n \circ s \circ n$ is a section of $s$: $$\sigma: \prod_{a:\mathbb{Z}} n(s(n(s(a)))) = a$$ * A dependent product of identities representing that $n \circ s \circ n$ is a retracion of $s$: $$\rho: \prod_{a:\mathbb{Z}} s(n(s(n(a)))) = a$$ * A dependent product of identities representing the coherence condition: $$\kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)$$ ### Definition 5 ### The integers are defined as the [[higher inductive type]] generated by: * A function $inj : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{Z}$. * A dependent product of functions between identities representing that equivalent differences are equal: $$equivdiff : \prod_{a:\mathbb{N}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{N}} \prod_{d:\mathbb{N}} (a + d = c + b) \to (inj(a,b) = inj(c,d))$$ * A set-truncator $$\tau_0: \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} isProp(a=b)$$ ## Properties ## TODO: Show that the integers are a ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the integers are initial in the category of ordered Heyting integral domains. ### Commutative ring structure on the integers ### We assume in this section that the integers are defined according to definition 1. +--{: .num_defn} ###### Definition The integer **zero** $0:\mathbb{Z}$ is defined as $$0 \coloneqq inj(0, 0)$$ =-- +--{: .num_defn} ###### Definition The binary operation **addition** $(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is inductively defined as $$inj(0,a) + inj(0,b) \coloneqq inj(0,a+b)$$ $$inj(1,a) + inj(1,b) \coloneqq inj(1,a+b)$$ $$inj(0,0) + inj(1,a) \coloneqq inj(1,a)$$ $$inj(0,a) + inj(1,0) \coloneqq inj(0,a)$$ $$inj(0,s(a)) + inj(1,s(b)) \coloneqq inj(0,a) + inj(1,b)$$ $$inj(1,0) + inj(0,a) \coloneqq inj(0,a)$$ $$inj(1,a) + inj(0,0) \coloneqq inj(1,a)$$ $$inj(1,s(a)) + inj(0,s(b)) \coloneqq inj(1,a) + inj(0,b)$$ for $a:\mathbb{N}$, $b:\mathbb{N}$, $(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$, $s:\mathbb{N} \to \mathbb{N}$. =-- +--{: .num_defn} ###### Definition The unary operation **negation** $-(-):\mathbb{Z} \to \mathbb{Z}$ is defined as $$-inj(a, b) \coloneqq inj(\neg a, b)$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $\neg:\mathbf{2} \to \mathbf{2}$ =-- +--{: .num_defn} ###### Definition The binary operation **subtraction** $(-)-(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as $$inj(a, b) - inj(c, d) \coloneqq inj(a, b) + inj(\neg c, d)$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The integer number **one** $1:\mathbb{Z}$ is defined as $$1 \coloneqq inj(0,1)$$ =-- +--{: .num_defn} ###### Definition The binary operation **multiplication** $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as $$inj(a,b) \cdot inj(c,d) \coloneqq inj(a \oplus c,b \cdot d)$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$, $(-)\cdot(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$, $(-)\oplus(-):\mathbf{2} \times \mathbf{2} \to \mathbf{2}$ (exclusive or binary operation in $\mathbf{2}$). =-- +--{: .num_defn} ###### Definition The right $\mathbb{N}$-action **exponentiation** $(-)^{(-)}:\mathbb{Z} \times \mathbb{N} \to \mathbb{Z}$ is inductively defined as $$inj(a,b)^0 \coloneqq inj(0,1)$$ $$inj(a,b)^{2n} \coloneqq inj(0,b^{2n})$$ $$inj(a,b)^{2n+1} \coloneqq inj(a,b^{2n+1})$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $n:\mathbb{N}$, $(-)^{(-)}:\mathbb{N} \times \mathbb{N} \to \mathbb{N}$. =-- ## See also ## * [[higher inductive type]] * [[rational numbers]] * [[decimal numbers]] * [[Eudoxus real numbers]] ## References ## [[HoTT book]] * Thorsten Altinkirch, _The Integers as a Higher Inductive Type_, ([abs:2007.00167](https://arxiv.org/abs/2007.00167)) * Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson, _Symmetry_, ([pdf](https://unimath.github.io/SymmetryBook/book.pdf))