[[!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 type 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}}$$ path application and recursion of interval $$\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}}{\Gamma, f:\mathbb{I} \to A \vdash \mathrm{rec}_\mathbb{I}^A(f(0), f(1), \mathrm{ap}_A(f)) \equiv f:\mathbb{I} \to A}$$ ... transport and type recursion of interval: $$\frac{\Gamma, x:\mathbb{I} \vdash A(x)}{\Gamma, f:\mathbb{I} \to \mathbb{I} \vdash \mathrm{tr}_{A(-)}(f):A(f(0)) \simeq A(f(1))}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma, x:\mathbb{I} \vdash \mathrm{rec}_\mathbb{I}^{A, B, e}(x) \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{rec}_\mathbb{I}^{A, B, e}(0) \equiv A \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{rec}_\mathbb{I}^{A, B, e}(1) \equiv B \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{tr}_{\mathrm{rec}_\mathbb{I}^{A, B, e}(-)}(\lambda i:\mathbb{I}.i) \equiv e:A \simeq B}$$ $$\frac{x:\mathbb{I} \vdash A(x)}{\Gamma, f:\mathbb{I} \to \mathbb{I}, x:\mathbb{I} \vdash A(x) \equiv \mathrm{rec}_\mathbb{I}^{A(f(0)), A(f(1)), \mathrm{tr}_{A(-)}(f)}(x) \; \mathrm{type}}$$ ... dependent path application and induction of interval: $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, f:\prod_{x:\mathbb{I}} A(x) \vdash \mathrm{apd}_{A(-)}(f):\mathrm{tr}_{A(-)}(\lambda i:\mathbb{I}.i)(f(0)) =_{A(1)} f(1)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type} \quad \Gamma \vdash x:A(0) \quad \Gamma \vdash y:A(1) \quad \Gamma \vdash p:\mathrm{tr}_{A(-)}(\lambda i:\mathbb{I}.i)(x) =_{A(1)} y}{\Gamma \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} \quad \Gamma \vdash x:A(0) \quad \Gamma \vdash y:A(1) \quad \Gamma \vdash p:\mathrm{tr}_{A(-)}(\lambda i:\mathbb{I}.i)(x) =_{A(1)} y}{\Gamma \vdash \mathrm{ind}_\mathbb{I}^{A(-)}(x, y, p)(0) \equiv x:A(0)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type} \quad \Gamma \vdash x:A(0) \quad \Gamma \vdash y:A(1) \quad \Gamma \vdash p:\mathrm{tr}_{A(-)}(\lambda i:\mathbb{I}.i)(x) =_{A(1)} y}{\Gamma \vdash \mathrm{ind}_\mathbb{I}^{A(-)}(x, y, p)(1) \equiv y:A(1)}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type} \quad \Gamma \vdash x:A(0) \quad \Gamma \vdash y:A(1) \quad \Gamma \vdash p:\mathrm{tr}_{A(-)}(\lambda i:\mathbb{I}.i)(x) =_{A(1)} y}{\Gamma \vdash \mathrm{apd}_{A(-)}(\mathrm{ind}_\mathbb{I}^{A(-)}(x, y, p)) \equiv p:\mathrm{tr}_{A(-)}(\lambda i:\mathbb{I}.i)(x) =_{A(1)} y}$$ $$\frac{\Gamma, x:\mathbb{I} \vdash A(x) \; \mathrm{type}}{\Gamma, f:\prod_{x:\mathbb{I}} A(x) \vdash \mathrm{ind}_\mathbb{I}^{A(-)}(f(0), f(1), \mathrm{apd}_{A(-)}(f)):\prod_{x:\mathbb{I}} A(x)}$$ .... Path induction: $$\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)}$$ ---- category: redirected to nlab