[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] --- **[[type formation rules]]** for the empty type $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \emptyset \; \mathrm{type}}$$ \linebreak **fiberwise elimination rules** for the empty type: $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \emptyset \quad \Gamma \vdash b:\emptyset \end{array} }{\Gamma \vdash \mathrm{ind}_\emptyset^{C}(f, b):C}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \emptyset \quad \Gamma \vdash b:\emptyset \end{array} }{\Gamma \vdash \mathrm{ind}_\emptyset^{C, \mathrm{sec}}(f, b):f(\mathrm{ind}_\emptyset^{C}(f, b)) =_\emptyset b}$$ The usual induction rules are given for $C \equiv \sum_{x:\emptyset} P(x)$ --- **[[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)$ --- Interval types, path types, and identity types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}$$ $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, f:\mathbb{I} \to A \vdash \mathrm{ap}_A(f):f(0) =_A f(1)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A, p:x =_A y \vdash \mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A, p:x =_A y \vdash \mathrm{rec}_\mathbb{I}^A(x, y, p)(0) \equiv x:A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A, p:x =_A y \vdash \mathrm{rec}_\mathbb{I}^A(x, y, p)(1) \equiv y:A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A, p:x =_A y \vdash \mathrm{ap}_{A}(\mathrm{rec}_\mathbb{I}^A(x, y, p)) \equiv p:x =_A y}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\mathbb{I} \to A \vdash C(z) \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma \vdash \mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\mathbb{I} \to A \vdash C(z) \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma, x:A \vdash \mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t:C(\lambda i:\mathbb{I}.x)}$$ ... $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to \mathbb{I}, x:A(p(0)), y:A(p(1)) \vdash x =_A^{p} y \; \mathrm{type}}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to \mathbb{I}, f:\prod_{x:\mathbb{I}} A(x) \vdash \mathrm{apd}_A(p, f):f(p(0)) =_A f(p(1))}$$ ---- $$(-) \bullet (-):(x =_A y) \to (y =_A z) \to (x =_A z)$$ $$\mathrm{ap}_A(\lambda i:\mathbb{I}.x) \equiv\mathrm{id}_{x =_A z}$$ category: redirected to nlab