[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] **[[type formation rules]]** for the unit type $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Unit} \; \mathrm{type}}$$ \linebreak **[[term introduction rules]]** for the unit type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{pt}:\mathrm{Unit}}$$ \linebreak **fiberwise elimination rules** for the unit type: $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \Gamma \vdash b:\mathrm{Unit} \end{array} }{\Gamma \vdash \mathrm{ind}_\mathrm{Unit}^{C, \mathrm{sec}}(f, c, p, b):C}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \Gamma \vdash b:\mathrm{Unit} \end{array} }{\Gamma \vdash \mathrm{ind}_\mathrm{Unit}^{C, \mathrm{path}}(f, c, p, b):f(\mathrm{ind}_\mathrm{Unit}^{C, \mathrm{sec}}(f, c, p, b)) =_\mathrm{Unit} b}$$ **fiberwise computation rules** for the unit type: $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \end{array} }{\Gamma \vdash \beta_\mathrm{Unit}^{C, \mathrm{sec}, \mathrm{pt}}(f, c, p):\mathrm{ind}_\mathrm{Unit}^{C, \mathrm{sec}}(f, c, p, \mathrm{pt}) =_{C} c}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \end{array} }{\Gamma \vdash \beta_\mathrm{Unit}^{C, \mathrm{path}, \mathrm{pt}}(f, c, p):\mathrm{ind}_\mathrm{Unit}^{C, \mathrm{path}}(f, c, p, \mathrm{pt}) =_{f(-) =_\mathrm{Unit} \mathrm{pt}}^{\beta_\mathrm{Unit}^{C, \mathrm{sec}, \mathrm{pt}}(f, c, p)} p}$$ The usual induction rules are given for $C \equiv \sum_{x:\mathrm{Unit}} P(x)$ ---- $$c_s:\prod_{n:\mathbb{N}} \left(\sum_{z:C} f(z) =_\mathbb{N} n\right) \to \left(\sum_{z:C} f(z) =_\mathbb{N} s(n)\right)$$ By currying this is the same as $$c_s:\prod_{n:\mathbb{N}} \prod_{z:C} \left(f(z) =_\mathbb{N} n\right) \to \left(\sum_{z:C} f(z) =_\mathbb{N} s(n)\right)$$ and by the type theoretic axiom of choice this is the same as $$c_s:\prod_{n:\mathbb{N}} \prod_{y:C} \sum_{g:(f(y) =_\mathbb{N} n) \to C} \prod_{p:f(y) =_\mathbb{N} n} f(g(p)) =_\mathbb{N} s(n)$$ The family of dependent sum types could be split up into $$c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C$$ $$p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n)$$ Then the fiberwise induction principle of the natural numbers states that given a type $C$ and a function $f:C \to \mathbb{N}$, along with * an element $c_0:C$ * an identification $p_0:f(c_0) =_\mathbb{N} 0$ * dependent functions $$c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C$$ $$p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n)$$ * a natural number $n:\mathbb{N}$ we have an element $$\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n):C$$ and an identification $$\mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, n):f(\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n)) =_\mathbb{N} n$$ such that **judgmental computation rules $$\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, 0) \equiv c_0$$ $$\mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, 0) \equiv p_0$$ and for all $n:\mathbb{N}$, $$\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, s(n)) \equiv c_s(n, \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, n))$$ $$\mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, s(n)) \equiv p_s(n, \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, n))$$ **typal computation rules** $$\beta_\mathbb{N}^{C, \mathrm{sec}, 0}(f, c_0, p_0, c_s, p_s):\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, 0) =_{C} c_0$$ $$\beta_\mathbb{N}^{C, \mathrm{path}, 0}(f, c_0, p_0, c_s, p_s):\mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, 0) =_{f(-) =_\mathbb{N} 0}^{\beta_\mathbb{N}^{C, \mathrm{sec}, 0}(f, c_0, p_0, c_s, p_s)} p_0$$ and for all $n:\mathbb{N}$, $$\beta_\mathbb{N}^{C, \mathrm{sec}, s}(f, c_0, p_0, c_s, p_s):\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, s(n)) =_{C} c_s(n, \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, n))$$ $$\beta_\mathbb{N}^{C, \mathrm{path}, 0}(f, c_0, p_0, c_s, p_s):\mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, s(n)) =_{f(-) =_\mathbb{N} s(n)}^{\beta_\mathbb{N}^{C, \mathrm{sec}, s}(f, c_0, p_0, c_s, p_s)} p_s(n, \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{path}}(f, c_0, p_0, c_s, p_s, n))$$ category: redirected to nlab