#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. We assume in this section that the integers are defined according to definition 1. ### Commutative ring structure on the integers ### +--{: .num_defn} ###### Definition The integer **zero** $0:\mathbb{Z}$ is defined as $$0 \coloneqq inj(0, 0)$$ =-- +--{: .num_defn} ###### Definition Let $(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be addition of the natural numbers, let $\rho:\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be the symmetric difference or metric of the natural numbers, and let $\lt:\mathbb{N} \times \mathbb{N} \to \mathbb{2}$ be the decidable strict order on the natural numbers into the booleans. 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,a) + inj(1,b) \coloneqq inj(a \lt b,\rho(a,b))$$ $$inj(1,a) + inj(0,b) \coloneqq inj(b \lt a,\rho(a,b))$$ for $a:\mathbb{N}$, $b:\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}$. =-- ### Order structure on the integers ### +--{: .num_defn} ###### Definition The dependent type *is positive*, denoted as $isPositive(inj(a,b))$, is defined as $$isPositive(inj(a,b)) \coloneqq (a = 0) \times (b \gt 0)$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, dependent types $m\gt n$ indexed by $m, n:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is negative*, denoted as $isNegative(inj(a,b))$, is defined as $$isPositive(inj(a,b)) \coloneqq (a = 1) \times (b \gt 0)$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, dependent types $m\gt n$ indexed by $m, n:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is zero*, denoted as $isZero(inj(a,b))$, is defined as $$isZero(inj(a,b)) \coloneqq b = 0$$ for $a:\mathbf{2}$, $b:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-positive*, denoted as $isNonPositive(inj(a,b))$ is defined as $$isNonPositive(inj(a,b)) \coloneqq isPositive(inj(a,b)) \to \emptyset$$ for $a:\mathbf{2}$, $b:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-negative*, denoted as $isNonNegative(inj(a,b))$, is defined as $$isNonNegative(inj(a,b)) \coloneqq isNegative(inj(a,b)) \to \emptyset$$ for $a:\mathbf{2}$, $b:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-zero*, denoted as $isNonZero(inj(a,b))$, is defined as $$isNonZero(inj(a,b)) \coloneqq \Vert isPositive(inj(a,b)) + isNegative(inj(a,b)) \Vert$$ for $a:\mathbf{2}$, $b:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is less than*, denoted as $inj(a,b) \lt inj(c,d)$, is defined as $inj(a,b) \lt inj(c,d) \coloneqq isPositive(inj(c,d) - inj(a,b))$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is greater than*, denoted as $inj(a,b) \gt inj(c,d)$, is defined as $inj(a,b) \gt inj(c,d) \coloneqq isNegative(inj(c,d) - inj(a,b))$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is apart from*, denoted as $inj(a,b) # inj(c,d)$, is defined as $inj(a,b) # inj(c,d) \coloneqq isNonZero(inj(c,d) - inj(a,b))$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is less than or equal to*, denoted as $inj(a,b) \leq inj(c,d)$, is defined as $inj(a,b) \leq inj(c,d) \coloneqq isNonNegaitve(inj(c,d) - inj(a,b))$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The dependent type *is greater than or equal to*, denoted as $inj(a,b) \geq inj(c,d)$, is defined as $inj(a,b) \geq inj(c,d) \coloneqq isNonPositive(inj(c,d) - inj(a,b))$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- ### Pseudolattice structure on the integers ### +--{: .num_defn} ###### Definition The **ramp function** $ramp:\mathbb{Z} \to \mathbb{Z}$ is inductively defined as $$ramp(inj(0, a)) \coloneqq inj(0, a)$$ $$ramp(inj(1, a)) \coloneqq 0$$ for $a:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The **minimum** $min:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as $$min(inj(a,b),inj(c,d)) \coloneqq inj(a,b) - ramp(inj(a,b) - inj(c,d))$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The **maximum** $max:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as $$max(inj(a,b),inj(c,d)) \coloneqq inj(a,b) + ramp(inj(c,d) - inj(a,b))$$ for $a:\mathbf{2}$, $b:\mathbb{N}$, $c:\mathbf{2}$, $d:\mathbb{N}$. =-- +--{: .num_defn} ###### Definition The **absolute value** $\vert(-)\vert:\mathbb{Z} \to \mathbb{Z}$ is defined as $$\vert inj(a,b) \vert \coloneqq max(inj(a,b), -inj(a,b))$$ for $a:\mathbf{2}$, $b:\mathbb{N}$. =-- ### Division and remainder ### +--{: .num_defn} ###### Definition **Integer division** $(-)\div(-):\mathbb{Z} \times \mathbb{Z}_{\neq 0} \to \mathbb{Z}$ is defined as $$inj(0,a) \div inj(0,b) \coloneqq inj(0,a \div b)$$ $$inj(0,a) \div inj(1,b) \coloneqq inj(1,a \div b)$$ $$inj(1,a) \div inj(0,b) \coloneqq inj(1,a \div b)$$ $$inj(1,a) \div inj(1,b) \coloneqq inj(0,a \div b)$$ for $a:\mathbb{N}$, $b:\mathbb{N}_{\neq 0}$. =-- ## Properties ## The integers are sequentially Cauchy complete with respect to the distance function defined as $d(x, y) \coloneqq \vert x - y \vert$. This is because any Cauchy sequence in the integers converges to an integer $n$ and only has a finite number of terms that are not equal to $n$. This is because the integers are not dense. ## See also ## * [[natural numbers]] * [[higher inductive type]] * [[rational numbers]] * [[decimal numbers]] * [[Eudoxus real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * 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)) category: not redirected to nlab yet