[[!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)}$$ ... need type recursion: $$\frac{\Gamma, x:\mathbb{I} \vdash A(x)}{\Gamma, f:\mathbb{I} \to \mathbb{I} \vdash \mathrm{tr}_{A(-)}(f):A(f(0)) \to A(f(1))}$$ $$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:A \vdash f(g(y)) \equiv y:B \end{array} }{\Gamma, x:\mathbb{I} \vdash \mathrm{typerec}_\mathbb{I}^{A, B, f, g}(x) \; \mathrm{type}}$$ $$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:A \vdash f(g(y)) \equiv y:B \end{array} }{\Gamma \vdash \mathrm{typerec}_\mathbb{I}^{A, B, f, g}(0) \equiv A \; \mathrm{type}}$$ $$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:A \vdash f(g(y)) \equiv y:B \end{array} }{\Gamma \vdash \mathrm{typerec}_\mathbb{I}^{A, B, f, g}(1) \equiv B \; \mathrm{type}}$$ $$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:A \vdash f(g(y)) \equiv y:B \end{array} }{\Gamma \vdash \mathrm{tr}_{A, B, f, g}:\mathrm{typerec}_\mathbb{I}^{A, B, f, g}(0) \to \mathrm{typerec}_\mathbb{I}^{A, B, f, g}(1) \; \mathrm{type}}$$ $$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:A \vdash f(g(y)) \equiv y:B \end{array} }{\Gamma \vdash \mathrm{tr}_{A, B, f, g}^{-1}:\mathrm{typerec}_\mathbb{I}^{A, B, f, g}(1) \to \mathrm{typerec}_\mathbb{I}^{A, B, f, g}(0) \; \mathrm{type}}$$ ---- ... $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, x:A(0), y:A(1) \vdash x =_{A(-)} y \; \mathrm{type}}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, f:\prod_{x:\mathbb{I}} A(x) \vdash \mathrm{apd}_A(f):f(0) =_{A(-)} f(1)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, x:A(0), y:A(1), p:x =_{A(-)} y \vdash \mathrm{ind}_\mathbb{I}^{A(-)}(x, y, p):\prod_{x:\mathbb{I}} A(x)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, x:A(0), y:A(1), p:x =_{A(-)} y \vdash \mathrm{ind}_\mathbb{I}^{A(-)}(x, y, p)(0) \equiv x:A(0)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, x:A(0), y:A(1), p:x =_{A(-)} y \vdash \mathrm{ind}_\mathbb{I}^{A(-)}(x, y, p)(1) \equiv y:A(1)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, x:A(0), y:A(1), p:x =_{A(-)} y \vdash \mathrm{apd}_{A}(\mathrm{ind}_\mathbb{I}^A(x, y, p)) \equiv p:x =_{A(-)} y}$$ ... $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, f:\mathbb{I} \to \mathbb{I}, x:A(f(0)), y:A(f(1)) \vdash x =_{A(-)}^{f} y \; \mathrm{type}}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, j:\mathbb{I}, x:A(j), \vdash x =_{A(-)}^{\lambda i:\mathbb{I}.j} x \; \mathrm{type}}$$ ---- $$(-) \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