[proofplan]
We prove the proposition by dependent elimination on the Sigma term $p$. The motive is the family of identity types asserting that $p$ is equal to the pair reconstructed from its two projections. In the constructor case $p=(a,b)$, the Sigma beta rules identify the two projections with $a$ and $b$, so the target identity reduces to reflexivity.
[/proofplan]
[step:Define the dependent motive for Sigma elimination]
Define the dependent predicate
\begin{align*}
C:\left(\Sigma_{x:A}B(x)\right)\to\mathsf{Type}
\end{align*}
by assigning to each $p:\Sigma_{x:A}B(x)$ the type
\begin{align*}
C(p)\coloneqq \operatorname{Id}_{\Sigma_{x:A}B(x)}\bigl(p,(\pi_1(p),\pi_2(p))\bigr).
\end{align*}
The desired theorem is precisely the construction of a term of $C(p)$ for every $p:\Sigma_{x:A}B(x)$.
[/step]
[step:Reduce the construction to canonical dependent pairs]
By the Sigma-type elimination principle [citetheorem:9631], it is enough to construct, for every $a:A$ and every $b:B(a)$, a term of
\begin{align*}
C((a,b)).
\end{align*}
Expanding the definition of $C$, this target is
\begin{align*}
\operatorname{Id}_{\Sigma_{x:A}B(x)}\bigl((a,b),(\pi_1((a,b)),\pi_2((a,b)))\bigr).
\end{align*}
[guided]
We want to prove a statement about an arbitrary element
$p:\Sigma_{x:A}B(x)$. The appropriate method is Sigma elimination: instead of trying to inspect an arbitrary pair directly, we prove the desired family of propositions for a canonical constructor term.
The family of propositions being proved is the motive
\begin{align*}
C:\left(\Sigma_{x:A}B(x)\right)\to\mathsf{Type}.
\end{align*}
For a dependent pair $p:\Sigma_{x:A}B(x)$, this motive is defined by
\begin{align*}
C(p)\coloneqq \operatorname{Id}_{\Sigma_{x:A}B(x)}\bigl(p,(\pi_1(p),\pi_2(p))\bigr).
\end{align*}
Thus a term of $C(p)$ is exactly a path from $p$ to the pair reconstructed from its first and second projections.
The Sigma-type elimination principle [citetheorem:9631] applies to this dependent family $C$, because $C(p)$ is a type depending on $p:\Sigma_{x:A}B(x)$. It reduces the construction of a dependent function
\begin{align*}
\prod_{p:\Sigma_{x:A}B(x)} C(p)
\end{align*}
to the construction, for each $a:A$ and $b:B(a)$, of a term of
\begin{align*}
C((a,b)).
\end{align*}
After substituting the definition of $C$, this constructor-case target is
\begin{align*}
\operatorname{Id}_{\Sigma_{x:A}B(x)}\bigl((a,b),(\pi_1((a,b)),\pi_2((a,b)))\bigr).
\end{align*}
This is the only case that must be proved, because Sigma elimination says that every dependent pair is analyzed by its constructor form for purposes of defining dependent functions out of the Sigma type.
[/guided]
[/step]
[step:Use the Sigma beta rules to identify the reconstructed pair]
Fix $a:A$ and $b:B(a)$. By the Sigma beta rules [citetheorem:9629], the projections of the canonical pair satisfy
\begin{align*}
\pi_1((a,b)) \equiv a.
\end{align*}
and
\begin{align*}
\pi_2((a,b)) \equiv b.
\end{align*}
Therefore the reconstructed pair
\begin{align*}
(\pi_1((a,b)),\pi_2((a,b)))
\end{align*}
is definitionally equal to
\begin{align*}
(a,b).
\end{align*}
So the target type in the constructor case reduces to
\begin{align*}
\operatorname{Id}_{\Sigma_{x:A}B(x)}((a,b),(a,b)).
\end{align*}
[/step]
[step:Construct the constructor case by reflexivity and conclude]
The identity type has the reflexivity constructor. Applying it to the term
\begin{align*}
(a,b):\Sigma_{x:A}B(x)
\end{align*}
gives
\begin{align*}
\operatorname{refl}_{(a,b)}:\operatorname{Id}_{\Sigma_{x:A}B(x)}((a,b),(a,b)).
\end{align*}
By the computation from the preceding step, this is a term of $C((a,b))$. Sigma elimination therefore yields a dependent function
\begin{align*}
\eta_{\Sigma}:\prod_{p:\Sigma_{x:A}B(x)}\operatorname{Id}_{\Sigma_{x:A}B(x)}\bigl(p,(\pi_1(p),\pi_2(p))\bigr).
\end{align*}
Evaluating this dependent function at the given $p:\Sigma_{x:A}B(x)$ gives the required term
\begin{align*}
\eta_{\Sigma}(p):\operatorname{Id}_{\Sigma_{x:A}B(x)}\bigl(p,(\pi_1(p),\pi_2(p))\bigr).
\end{align*}
[/step]
