#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. ## See also ## * [[higher inductive type]] * [[rational numbers]] * [[decimal 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))