[[!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)$ --- There is a version of the induction principle which uses a type $C$ and a function $f:C \to \sum_{x:A} \sum_{y:A} x =_A y$ instead of a type family $C(x, y, p)$ indexed by $x:A$, $y:A$, and $p:x =_A y$. Let $$\Delta_A \coloneqq \lambda x:A.(x, x, \mathrm{refl}_A(x)):A \to \sum_{x:A} \sum_{y:A} x =_A y$$ be the [[diagonal function]] of $A$. The induction principle for the identity type says that given any type $C$ and function $$f:C \to \sum_{x:A} \sum_{y:A} x =_A y$$ into the type of all identity types in $A$, and given a function $c:A \to C$ and a homotopy $$p:\prod_{x:A} f(c(x)) =_{\sum_{x:A} \sum_{y:A} x =_A y} \Delta_A(x)$$ which states that the composite of $f$ and $c$ is the diagonal, one can construct * a function $$g:\left(\sum_{x:A} \sum_{y:A} x =_A y\right) \to C$$ * a homotopy witnessing that $g$ is a [[section]] of $f$: $$\mathrm{sec}_g:\prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} f(g(z)) =_{\sum_{x:A} \sum_{y:A} x =_A y} z$$ such that for all $x:A$, $g(\Delta_A(x)) \equiv c(x)$ and $\mathrm{sec}_g(\Delta_A(x)) \equiv p$. category: redirected to nlab