[[!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)$ category: redirected to nlab