[proofplan]
We prove the result by the standard encode-decode method for identity types. First we define the forward map by path induction on a path between Sigma-pairs, so the reflexive path is encoded by the reflexive base path together with the reflexive fiber path. Then we define the inverse by induction on the base path and then on the fiber path. Finally, the two composite maps are shown to be homotopic to the identity by the same induction principles, and these homotopies package the two maps as an equivalence.
[/proofplan]
[step:Define the code type and encode paths between dependent pairs]
Let
\begin{align*}
S := \sum_{z:A} B(z).
\end{align*}
For $x=(a,u):S$ and $y=(b,v):S$, define
\begin{align*}
\operatorname{Code}(x,y) := \sum_{p:\operatorname{Id}_A(a,b)} \operatorname{Id}_{B(b)}\bigl(\operatorname{transport}^{B}(p)(u),v\bigr).
\end{align*}
We define a function
\begin{align*}
\operatorname{encode}_{x,y}:\operatorname{Id}_{S}(x,y)\to \operatorname{Code}(x,y)
\end{align*}
by path induction on $r:\operatorname{Id}_{S}(x,y)$, using the [[path induction principle](/theorems/9633)][citetheorem:9633]. It is therefore enough to define the value when $y\equiv x$ and $r\equiv \operatorname{refl}_x$. Writing $x=(a,u)$, the reflexive case has target
\begin{align*}
\operatorname{Code}(x,x)=\sum_{p:\operatorname{Id}_A(a,a)} \operatorname{Id}_{B(a)}\bigl(\operatorname{transport}^{B}(p)(u),u\bigr).
\end{align*}
By the reflexive computation rule for transport, stated in the [Transport Lemma][citetheorem:9634],
\begin{align*}
\operatorname{transport}^{B}(\operatorname{refl}_a)(u)\equiv u.
\end{align*}
Hence we set
\begin{align*}
\operatorname{encode}_{x,x}(\operatorname{refl}_x) := (\operatorname{refl}_a,\operatorname{refl}_u).
\end{align*}
This determines $\operatorname{encode}_{x,y}$ for all $x,y:S$ and all paths $r:\operatorname{Id}_S(x,y)$.
[guided]
The target of the forward map records exactly the data contained in a path between dependent pairs: first a path between first components, and then a path between second components after transporting along that first path. For $x=(a,u):S$ and $y=(b,v):S$, this target is the type
\begin{align*}
\operatorname{Code}(x,y) := \sum_{p:\operatorname{Id}_A(a,b)} \operatorname{Id}_{B(b)}\bigl(\operatorname{transport}^{B}(p)(u),v\bigr).
\end{align*}
We now define
\begin{align*}
\operatorname{encode}_{x,y}:\operatorname{Id}_{S}(x,y)\to \operatorname{Code}(x,y).
\end{align*}
The input is a path $r:\operatorname{Id}_S(x,y)$ between elements of the Sigma type $S$. By the [path induction principle][citetheorem:9633], to define a dependent function out of such paths, it is enough to define it on the reflexive path. Thus we reduce to the case $y\equiv x$ and $r\equiv \operatorname{refl}_x$.
Write $x=(a,u)$, where $a:A$ and $u:B(a)$. In the reflexive case the code type is
\begin{align*}
\operatorname{Code}(x,x)=\sum_{p:\operatorname{Id}_A(a,a)} \operatorname{Id}_{B(a)}\bigl(\operatorname{transport}^{B}(p)(u),u\bigr).
\end{align*}
The natural first component is the reflexive path $\operatorname{refl}_a:\operatorname{Id}_A(a,a)$. With this choice, the second component must have type
\begin{align*}
\operatorname{Id}_{B(a)}\bigl(\operatorname{transport}^{B}(\operatorname{refl}_a)(u),u\bigr).
\end{align*}
By the reflexive computation rule for transport in the [Transport Lemma][citetheorem:9634], transport along $\operatorname{refl}_a$ is judgmentally the identity on the fiber $B(a)$:
\begin{align*}
\operatorname{transport}^{B}(\operatorname{refl}_a)(u)\equiv u.
\end{align*}
So the required second component is simply $\operatorname{refl}_u$. Therefore the defining reflexive value is
\begin{align*}
\operatorname{encode}_{x,x}(\operatorname{refl}_x):=(\operatorname{refl}_a,\operatorname{refl}_u).
\end{align*}
This definition agrees with the informal description of the canonical map. The first component is the action of the first projection on paths, as supplied by [congruence of functions](/theorems/9635) in [citetheorem:9635], and the second component is the induced path in the transported fiber; path induction proves this identification because both descriptions reduce to $(\operatorname{refl}_a,\operatorname{refl}_u)$ in the reflexive case.
[/guided]
[/step]
[step:Construct the inverse path from a base path and a transported fiber path]
Fix $x=(a,u):S$ and $y=(b,v):S$. We define
\begin{align*}
\operatorname{pairpath}_{x,y}:\operatorname{Code}(x,y)\to \operatorname{Id}_{S}(x,y).
\end{align*}
An element of $\operatorname{Code}(x,y)$ is a pair $(p,q)$ with
\begin{align*}
p:\operatorname{Id}_A(a,b)
\end{align*}
and
\begin{align*}
q:\operatorname{Id}_{B(b)}\bigl(\operatorname{transport}^{B}(p)(u),v\bigr).
\end{align*}
We construct $\operatorname{pairpath}_{x,y}(p,q)$ by path induction on $p$. In the reflexive case $b\equiv a$ and $p\equiv\operatorname{refl}_a$, so $q$ has type $\operatorname{Id}_{B(a)}(u,v)$ by the reflexive transport computation. Applying path induction to $q$, it is enough to consider $v\equiv u$ and $q\equiv\operatorname{refl}_u$, where we define
\begin{align*}
\operatorname{pairpath}_{(a,u),(a,u)}(\operatorname{refl}_a,\operatorname{refl}_u):=\operatorname{refl}_{(a,u)}.
\end{align*}
This defines the desired inverse candidate.
[/step]
[step:Show that decoding after encoding is the identity on paths between pairs]
We prove that for all $x,y:S$ and all $r:\operatorname{Id}_S(x,y)$,
\begin{align*}
\operatorname{pairpath}_{x,y}(\operatorname{encode}_{x,y}(r))=\operatorname{refl}_{\operatorname{Id}_S(x,y)}(r).
\end{align*}
By path induction on $r$, it suffices to consider $y\equiv x$ and $r\equiv\operatorname{refl}_x$. Writing $x=(a,u)$, the definitions give
\begin{align*}
\operatorname{encode}_{x,x}(\operatorname{refl}_x)=(\operatorname{refl}_a,\operatorname{refl}_u).
\end{align*}
The definition of $\operatorname{pairpath}$ then gives
\begin{align*}
\operatorname{pairpath}_{x,x}(\operatorname{refl}_a,\operatorname{refl}_u)=\operatorname{refl}_x.
\end{align*}
Thus the required equality is $\operatorname{refl}_{\operatorname{refl}_x}$ in the reflexive case, and path induction gives the homotopy for all $r$.
[/step]
[step:Show that encoding after decoding is the identity on codes]
We prove that for all $x=(a,u):S$, $y=(b,v):S$, and all $c:\operatorname{Code}(x,y)$,
\begin{align*}
\operatorname{encode}_{x,y}(\operatorname{pairpath}_{x,y}(c))=c.
\end{align*}
Write $c=(p,q)$, where
\begin{align*}
p:\operatorname{Id}_A(a,b)
\end{align*}
and
\begin{align*}
q:\operatorname{Id}_{B(b)}\bigl(\operatorname{transport}^{B}(p)(u),v\bigr).
\end{align*}
We apply path induction to $p$. In the reflexive case $b\equiv a$ and $p\equiv\operatorname{refl}_a$, the transport term reduces to $u$, so $q:\operatorname{Id}_{B(a)}(u,v)$. Applying path induction to $q$, it remains to prove the case $v\equiv u$ and $q\equiv\operatorname{refl}_u$. In that case,
\begin{align*}
\operatorname{pairpath}_{(a,u),(a,u)}(\operatorname{refl}_a,\operatorname{refl}_u)=\operatorname{refl}_{(a,u)}
\end{align*}
and then
\begin{align*}
\operatorname{encode}_{(a,u),(a,u)}(\operatorname{refl}_{(a,u)})=(\operatorname{refl}_a,\operatorname{refl}_u).
\end{align*}
Therefore the required equality reduces to the reflexivity path of $(\operatorname{refl}_a,\operatorname{refl}_u)$. The two inductions give the desired homotopy for all codes $c$.
[/step]
[step:Package the two maps as an equivalence]
For every $x=(a,u):S$ and $y=(b,v):S$, we have constructed maps
\begin{align*}
\operatorname{encode}_{x,y}:\operatorname{Id}_{S}(x,y)\to \operatorname{Code}(x,y)
\end{align*}
and
\begin{align*}
\operatorname{pairpath}_{x,y}:\operatorname{Code}(x,y)\to \operatorname{Id}_{S}(x,y).
\end{align*}
The previous two steps give homotopies
\begin{align*}
\operatorname{pairpath}_{x,y}\circ \operatorname{encode}_{x,y}\sim \operatorname{id}_{\operatorname{Id}_S(x,y)}
\end{align*}
and
\begin{align*}
\operatorname{encode}_{x,y}\circ \operatorname{pairpath}_{x,y}\sim \operatorname{id}_{\operatorname{Code}(x,y)}.
\end{align*}
Thus $\operatorname{encode}_{x,y}$ has $\operatorname{pairpath}_{x,y}$ as a two-sided inverse up to identity, so $\operatorname{encode}_{x,y}$ is an equivalence. This is exactly the asserted characterization of the identity type of the Sigma type $S=\sum_{z:A}B(z)$.
[/step]
