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