[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ### Double induction $$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} C(m, n)}$$ $$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, 0, 0}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, 0) =_{C(0, 0)} c_{0, 0}}$$ $$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, 0, s}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{n:\mathbb{Z}} \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, s(n)) =_{C(0, s(n))} c_{0, s}(n, \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, n))}$$ $$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, s, 0}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{n:\mathbb{Z}} \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, s(n), 0) =_{C(s(n), 0)} c_{s, 0}(n, \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, n, 0))}$$ $$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, s, s}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, s(m), s(n)) =_{C(s(m), s(n))} c_{0, s}(m, n, \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, m, n))}$$ ### Double recursion The rules for double recursion are the following: $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C \quad \Gamma \vdash c_{0, s}:\mathbb{Z} \to (C \simeq C) \\ \Gamma \vdash c_{s, 0}:\mathbb{Z} \to (C \simeq C) \quad \Gamma \vdash c_{s, s}:(\mathbb{Z} \times \mathbb{Z}) \to (C \simeq C) \end{array} }{\Gamma \vdash \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):(\mathbb{Z} \times \mathbb{Z}) \to C}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C \quad \Gamma \vdash c_{0, s}:\mathbb{Z} \to (C \simeq C) \\ \Gamma \vdash c_{s, 0}:\mathbb{Z} \to (C \simeq C) \quad \Gamma \vdash c_{s, s}:(\mathbb{Z} \times \mathbb{Z}) \to (C \simeq C) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, 0, 0}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, 0) =_{C} c_{0, 0}}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C \quad \Gamma \vdash c_{0, s}:\mathbb{Z} \to (C \simeq C) \\ \Gamma \vdash c_{s, 0}:\mathbb{Z} \to (C \simeq C) \quad \Gamma \vdash c_{s, s}:(\mathbb{Z} \times \mathbb{Z}) \to (C \simeq C) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, 0, s}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{n:\mathbb{Z}} \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, s(n)) =_{C} c_{0, s}(n, \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, n))}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C \quad \Gamma \vdash c_{0, s}:\mathbb{Z} \to (C \simeq C) \\ \Gamma \vdash c_{s, 0}:\mathbb{Z} \to (C \simeq C) \quad \Gamma \vdash c_{s, s}:(\mathbb{Z} \times \mathbb{Z}) \to (C \simeq C) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, s, 0}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{n:\mathbb{Z}} \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, s(n), 0) =_{C} c_{s, 0}(n, \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, n, 0))}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C \quad \Gamma \vdash c_{0, s}:\mathbb{Z} \to (C \simeq C) \\ \Gamma \vdash c_{s, 0}:\mathbb{Z} \to (C \simeq C) \quad \Gamma \vdash c_{s, s}:(\mathbb{Z} \times \mathbb{Z}) \to (C \simeq C) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, s, s}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, s(m), s(n)) =_{C} c_{0, s}(m, n, \mathrm{rec}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, m, n))}$$ ### Associative laws We define the associative laws by triple induction on the integers. We have $$x:\mathbb{Z}, z:\mathbb{Z}, \mathrm{ap}_{\lambda t:\mathbb{Z}.x + t}(0 + z, z, \mathrm{ind}_{\mathbb{Z}}^{x + (0 + z) =_{\mathbb{Z}} x + z}(\beta_\mathbb{Z}^{+, 0, 0}, \beta_\mathbb{Z}^{+, 0, s})):(x + (0 + z) =_\mathbb{Z} x + z)$$ and $$\mathrm{ap}_{\lambda t:\mathbb{Z}.t + 0}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0}):((0 + 0) + 0 =_\mathbb{Z} 0 + 0)$$ Thus, we have $$\mathrm{ap}_{\lambda t:\mathbb{Z}.0 + t}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0}) \bullet \mathrm{ap}_{\lambda t:\mathbb{Z}.t + 0}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0})^{-1}:(0 + (0 + 0) =_\mathbb{Z} (0 + 0) + 0)$$ We also have $$x:\mathbb{Z} \vdash \mathrm{ap}_{\lambda t:\mathbb{Z}.s(x) + t}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, s}):(s(x) + (0 + 0) =_\mathbb{Z} s(x) + 0)$$ and $$\mathrm{ap}_{\lambda x:\mathbb{Z}.x + 0}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0}):((0 + 0) + 0 =_\mathbb{Z} 0 + 0)$$ Thus, we have $$\mathrm{ap}_{\lambda x:\mathbb{Z}.0 + x}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0}) \bullet \mathrm{ap}_{\lambda x:\mathbb{Z}.x + 0}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0})^{-1}:(0 + (0 + 0) =_\mathbb{Z} (0 + 0) + 0)$$ We define the [[homotopies]] for the [[H-space]] structure of the integers type by induction on the integers type. For the case with the element $0:\mathbb{Z}$, one gets the identity $\beta_\mathbb{Z}^{+, 0, 0}:0 + 0 =_\mathbb{Z} 0$ from the rules for addition. For the case with the equivalence $s:\mathbb{Z} \simeq \mathbb{Z}$, the application to $s$ is itself a dependent function of a family of equivalences, $$\mathrm{ap}_{s}:\prod_{y:\mathbb{Z}} \prod_{x:\mathbb{Z}} (y =_\mathbb{Z} x) \simeq (s(y) =_\mathbb{Z} s(x))$$ Substituting $x + (y + z)$ and $(x + y) + z$ in for $y$ and $x$ respectively yields the family of equivalences $$x:\mathbb{Z}, y:\mathbb{Z}, z:\mathbb{Z} \vdash \mathrm{ap}_{s}(x + (y + z), (x + y) + z):(x + (y + z) =_\mathbb{Z} (x + y) + z) \simeq (s(x + (y + z)) =_\mathbb{Z} s((x + y) + z))$$ and by the [[introduction rule]] of [[dependent product types]], one gets the dependent functions of families of equivalences $$\lambda x:\mathbb{Z}.\lambda y:\mathbb{Z}.\lambda z:\mathbb{Z}.\mathrm{ap}_{s}(x + (y + z), (x + y) + z):\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} \prod_{z:\mathbb{Z}} (x + (y + z) =_\mathbb{Z} (x + y) + z) \simeq (s(x + (y + z)) =_\mathbb{Z} s((x + y) + z))$$ ### Inverse laws We define the [[homotopies]] for the [[H-space]] structure of the integers type by induction on the integers type. For the case with the element $0:\mathbb{Z}$, one gets the identity $\beta_\mathbb{Z}^{+, 0, 0}:0 + 0 =_\mathbb{Z} 0$ from the rules for addition. For the case with the equivalence $s:\mathbb{Z} \simeq \mathbb{Z}$, the application to $s$ is itself a dependent function of a family of equivalences, $$\mathrm{ap}_{s}:\prod_{y:\mathbb{Z}} \prod_{x:\mathbb{Z}} (y =_\mathbb{Z} x) \simeq (s(y) =_\mathbb{Z} s(x))$$ Substituting $x + -x$ and $-x + x$ in for $y$ and $0$ in for $x$ yields the family of equivalences $$x:\mathbb{Z} \vdash \mathrm{ap}_{s}(x + -x, 0):(x + -x =_\mathbb{Z} 0) \simeq (s(x + -x) =_\mathbb{Z} s(0))$$ $$x:\mathbb{Z} \vdash \mathrm{ap}_{s}(-x + x, 0):(-x + x =_\mathbb{Z} 0) \simeq (-x + x) =_\mathbb{Z} s(0))$$ and by the [[introduction rule]] of [[dependent product types]], one gets the dependent functions of families of equivalences $$\lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + -x, 0):\prod_{x:\mathbb{Z}} (x + -x =_\mathbb{Z} 0) \simeq (s(x + -x) =_\mathbb{Z} s(0))$$ $$\lambda x:\mathbb{Z}.\mathrm{ap}_{s}(-x + x, 0):\prod_{x:\mathbb{Z}} (-x + x =_\mathbb{Z} 0) \simeq (-x + x) =_\mathbb{Z} s(0))$$ category: redirected to nlab