[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Time to prove induction from the recursion. We begin with the simplest: the empty type. The recursion principle for the empty type says that for all types $A$ the type of functions $\emptyset \to A$ is contractible. Then the induction principle says that given a family of types $A(x)$ indexed by $x:\emptyset$ the dependent function type $\prod_{x:\emptyset} A(x)$ is contractible. But for any dependent function type $f:\prod_{x:\emptyset} A(x)$ one could construct the graph of the function $$\lambda x:\emptyset.(x, f(x)):\emptyset \to \sum_{x:\emptyset} A(x)$$ so it suffices to prove it for the graph of $f$. Similarly we have $$x:A, y:A \vdash \lambda p:x =_A y.(p, t(p)):(x =_A y) \to \sum_{p:x =_A y} C(x, y, p)$$ ---- For propositional interval type localization we prove the recursion and uniqueness principles: \begin{theorem} Suppose that every type $A$ is definitionally $\mathbb{I}$-local. Then path recursion for function types out of the interval type holds: given any type $A$, and any family $C$, and given any function $t:A \to C$, one can construct a unique function $\mathrm{rec}_{\mathbb{I} \to A}(t):\mathbb{I} \to A \to C$ with a homotopy $$\beta_{\mathbb{I} \to A}(t):\prod_{x:A} \mathrm{rec}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) =_{C} t(x)$$ \end{theorem} \begin{proof} $\mathrm{ind}_{\mathbb{I} \to A}(t)$ is defined to be $$\mathrm{ind}_{\mathbb{I} \to A}(t) \equiv \lambda p:\mathbb{I} \to A.t(\mathrm{const}_{A, \mathrm{I}}^{-1}(p))$$ and by the computation rules of path types as negative copies, one has that for all $x:A$, $$\beta_{\mathbb{I} \to A}:\prod_{x:A} \mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x) =_{A} x$$ and so by function application one has $$\mathrm{ap}_{t}(\beta_{\mathbb{I} \to A}(x)):t(\mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x)) =_C t(x)$$ and by definition of $\mathrm{ind}_{\mathbb{I} \to A}(t)$ and the judgmental congruence rules for substitution, one has $$\mathrm{ap}_{t}(\beta_{\mathbb{I} \to A}(x)):\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) =_C t(x)$$ \end{proof} category: redirected to nlab