[proofplan] The Sigma type $\Sigma_{x:A}B(x)$ is generated by one constructor, the dependent pair constructor $(x,y)$ with $x:A$ and $y:B(x)$. Therefore a dependent function out of $\Sigma_{x:A}B(x)$ is defined by Sigma induction once its value has been specified on an arbitrary introduced pair. We use the given term $g(x,y):C((x,y))$ as exactly that constructor case, and the beta rule for the Sigma eliminator gives the stated judgmental computation rule. [/proofplan] [step:Apply Sigma induction using the given constructor case] Let $A$ be a type, let $B:A\to\mathsf{Type}$ be a type family, and let \begin{align*} C:\left(\Sigma_{x:A}B(x)\right)\to\mathsf{Type} \end{align*} be the target family. Suppose \begin{align*} g:\prod_{x:A}\prod_{y:B(x)} C((x,y)) \end{align*} is given. The dependent eliminator for Sigma types states that, to construct a term of \begin{align*} \prod_{p:\Sigma_{x:A}B(x)} C(p), \end{align*} it is enough to give, for arbitrary $x:A$ and $y:B(x)$, a term of $C((x,y))$. The supplied function $g$ gives precisely such a term, namely $g(x,y):C((x,y))$. Define \begin{align*} f:\prod_{p:\Sigma_{x:A}B(x)} C(p) \end{align*} to be the Sigma eliminator applied to this constructor case $g$. [guided] We want to define a dependent function whose input is an arbitrary dependent pair \begin{align*} p:\Sigma_{x:A}B(x). \end{align*} Because the codomain depends on the input, the desired output type is not fixed once and for all; at the input $p$, the output must have type $C(p)$. The Sigma type has one constructor: from $x:A$ and $y:B(x)$ it forms the pair \begin{align*} (x,y):\Sigma_{x:A}B(x). \end{align*} The dependent eliminator for Sigma types says that a definition on all elements of $\Sigma_{x:A}B(x)$ is obtained by giving the value on this constructor form. Thus the required constructor case has type \begin{align*} \prod_{x:A}\prod_{y:B(x)} C((x,y)). \end{align*} This is exactly the type of the given function $g$. For each $x:A$ and $y:B(x)$, the term $g(x,y)$ has type $C((x,y))$, which is the target family $C$ evaluated at the introduced pair. Therefore Sigma induction defines a dependent function \begin{align*} f:\prod_{p:\Sigma_{x:A}B(x)} C(p). \end{align*} Concretely, this $f$ is the eliminator for $\Sigma_{x:A}B(x)$ with motive $C$ and constructor branch $g$. [/guided] [/step] [step:Use the Sigma beta rule on introduced pairs] Let $a:A$ and $b:B(a)$. Since $f$ was defined by the Sigma eliminator with constructor branch $g$, the beta computation rule for Sigma elimination gives \begin{align*} f((a,b)) \equiv g(a,b):C((a,b)). \end{align*} This is exactly the stated computation rule. Hence the dependent function $f$ exists with the required behavior on every introduced pair, completing the proof. [/step]