[[!redirects integers > history]] [[!redirects integers]] < [[nlab:integer]] ## Definition The integers $\mathbb{Z}$ are the initial commutative ring structure on the natural numbers $\mathbb{N}$. A commutative ring structure on $\mathbb{N}$ consists of an element $1:\mathbb{N}$, functions $(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ and $(-)\cdot(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$, and dependent products $$\mathrm{assoc}_+:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x + (y + z) =_\mathbb{N} (x + y) + z$$ $$\mathrm{linv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.x + y)$$ $$\mathrm{rinv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.y + x)$$ $$\mathrm{ldist}_{\cdot, +}:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x \cdot (y + z) =_\mathbb{N} x \cdot y + x \cdot z$$ $$\mathrm{rdist}_{\cdot, +}:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} (y + z) \cdot x =_\mathbb{N} y \cdot x + z \cdot x$$ $$\mathrm{lunit}_{\cdot, 1}:\prod_{x:\mathbb{N}} 1 \cdot x =_\mathbb{N} x$$ $$\mathrm{runit}_{\cdot, 1}:\prod_{x:\mathbb{N}} x \cdot 1 =_\mathbb{N} x$$ $$\mathrm{comm}_{\cdot}:\prod_{x:\mathbb{N}} x \cdot y =_\mathbb{N} y \cdot x$$ The type of all commutative ring structures on $\mathbb{N}$ is given by $$\mathrm{CRingStr}(\mathbb{N}) \coloneqq \begin{array}{c} \sum_{1:\mathbb{N}} \sum_{+:\mathbb{N} \times \mathbb{N} \to \mathbb{N}} \sum_{\cdot:\mathbb{N} \times \mathbb{N} \to \mathbb{N}} \left(\prod_{x:\mathbb{N}} \prod_{y:v} \prod_{z:\mathbb{N}} x + (y + z) =_\mathbb{N} (x + y) + z\right) \\ \times \left(\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.x + y)\right) \times \left(\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.y + x)\right) \\ \times \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x \cdot (y + z) =_\mathbb{N} x \cdot y + x \cdot z\right) \times \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} (y + z) \cdot x =_\mathbb{N} y \cdot x + z \cdot x\right) \\ \times \left(\prod_{x:\mathbb{N}} 1 \cdot x =_\mathbb{N} x\right) \times \left(\prod_{x:R} x \cdot 1 =_\mathbb{N} x\right) \times \left(\prod_{x:R} x \cdot y =_\mathbb{N} y \cdot x\right) \end{array} $$ A commutative ring homomorphism between two commutative ring structures $A:\mathrm{CRingStr}(\mathbb{N})$ and $B:\mathrm{CRingStr}(\mathbb{N})$ consists of a function $f:\mathbb{N} \to \mathbb{N}$ and dependent products $$\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x +_A y) =_\mathbb{N} f(x) +_B f(y)$$ $$\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x \cdot_A y) =_\mathbb{N} f(x) \cdot_B f(y)$$ $$f(1_A) =_\mathbb{N} 1_B$$ The type of commutative ring homomorphisms between commutative ring structures $A:\mathrm{CRingStr}(\mathbb{N})$ and $B:\mathrm{CRingStr}(\mathbb{N})$ is given by $$\mathrm{CRingHom}(\mathbb{N})(A, B) \coloneqq \begin{array}{c} \sum_{f:\mathbb{N} \to \mathbb{N}} \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x +_A y) =_\mathbb{N} f(x) +_B f(y)\right) \\ \times \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x \cdot_A y) =_\mathbb{N} f(x) \cdot_B f(y)\right) \times \left(f(1_A) =_S 1_B\right) \end{array} $$ The initial commutative ring structure on $\mathbb{N}$ is a commutative ring structure $\mathbb{Z}:\mathrm{CRingStr}(\mathbb{N})$ such that for all commutative ring structures $R:\mathrm{CRingStr}(\mathbb{N})$ the type of commutative ring homomorphisms $\mathrm{CRingHom}(\mathbb{N})(\mathbb{Z}, R)$ is contractible: $$\sum_{\mathbb{Z}:\mathrm{CRingStr}(\mathbb{N})} \prod_{R:\mathrm{CRingStr}(\mathbb{N})} \mathrm{isContr}(\mathrm{CRingHom}(\mathbb{N})(\mathbb{Z}, R))$$ category: redirected to nlab