[proofplan]
We define the reassociation map from left to right by sending a nested dependent pair $(x,(y,z))$ to the dependent pair $((x,y),z)$. We define the inverse map from right to left by sending $(p,z)$ to $(\pi_1(p),(\pi_2(p),z))$. The left composite reduces to the identity by the Sigma beta rules, and the right composite is proved by Sigma elimination on the intermediate pair $p$, reducing it to the same beta computation. These two maps and their two identity homotopies are precisely the inverse data required for an equivalence.
[/proofplan]
[step:Define the two reassociation maps between the iterated Sigma types]
Define the source type $L$ and the target type $R$ by
\begin{align*}
L := \Sigma_{x:A}\Sigma_{y:B(x)}C(x,y)
\end{align*}
and
\begin{align*}
R := \Sigma_{p:\Sigma_{x:A}B(x)} C(\pi_1(p),\pi_2(p)).
\end{align*}
We define a function
\begin{align*}
F : L \to R
\end{align*}
by Sigma elimination as follows. For $x:A$, $y:B(x)$, and $z:C(x,y)$, set
\begin{align*}
F(x,(y,z)) := ((x,y),z).
\end{align*}
This is well-typed because $(x,y):\Sigma_{x:A}B(x)$ and, by the Sigma beta rules [citetheorem:9629],
\begin{align*}
\pi_1((x,y)) = x
\end{align*}
and
\begin{align*}
\pi_2((x,y)) = y.
\end{align*}
Thus $z:C(x,y)$ may be regarded as an element of $C(\pi_1((x,y)),\pi_2((x,y)))$.
Define a function
\begin{align*}
G : R \to L
\end{align*}
by
\begin{align*}
G(p,z) := (\pi_1(p),(\pi_2(p),z)).
\end{align*}
This is well-typed because $p:\Sigma_{x:A}B(x)$ gives $\pi_1(p):A$ and $\pi_2(p):B(\pi_1(p))$, while the second component $z$ has type $C(\pi_1(p),\pi_2(p))$.
[/step]
[step:Show that the composite from the left type to itself is the identity]
We prove that $G \circ F$ is homotopic to $\operatorname{id}_L$. By Sigma elimination on an arbitrary element of $L$, it is enough to consider an element of the form $(x,(y,z))$, where $x:A$, $y:B(x)$, and $z:C(x,y)$. Using the definitions of $F$ and $G$, we compute
\begin{align*}
G(F(x,(y,z))) = G((x,y),z).
\end{align*}
By the definition of $G$,
\begin{align*}
G((x,y),z) = (\pi_1((x,y)),(\pi_2((x,y)),z)).
\end{align*}
Applying the Sigma beta rules [citetheorem:9629] to the pair $(x,y)$ gives
\begin{align*}
(\pi_1((x,y)),(\pi_2((x,y)),z)) = (x,(y,z)).
\end{align*}
Therefore, for every $\ell:L$, there is a path
\begin{align*}
\eta_\ell : G(F(\ell)) = \ell.
\end{align*}
[guided]
The goal of this step is to verify one of the two inverse identities. Let
\begin{align*}
\ell : L
\end{align*}
be arbitrary. Since $L$ is a Sigma type whose elements are nested dependent pairs, Sigma elimination allows us to prove the desired identity by considering the general constructor form
\begin{align*}
\ell = (x,(y,z)),
\end{align*}
where $x:A$, $y:B(x)$, and $z:C(x,y)$.
Now compute the composite $G \circ F$ on this constructor form. The forward map first reassociates the pair:
\begin{align*}
F(x,(y,z)) = ((x,y),z).
\end{align*}
Applying $G$ to this result gives
\begin{align*}
G(F(x,(y,z))) = G((x,y),z).
\end{align*}
By the definition of $G$, this is
\begin{align*}
G((x,y),z) = (\pi_1((x,y)),(\pi_2((x,y)),z)).
\end{align*}
The only computation rule needed now is the Sigma beta rule [citetheorem:9629]. It says that the projections of a constructed pair recover its components:
\begin{align*}
\pi_1((x,y)) = x
\end{align*}
and
\begin{align*}
\pi_2((x,y)) = y.
\end{align*}
Substituting these two projection computations into the displayed expression gives
\begin{align*}
G(F(x,(y,z))) = (x,(y,z)).
\end{align*}
Thus the composite $G \circ F$ agrees with the identity on every constructor-generated element of $L$. By Sigma elimination, this yields a homotopy
\begin{align*}
\eta : \prod_{\ell:L} G(F(\ell)) = \ell.
\end{align*}
[/guided]
[/step]
[step:Show that the composite from the right type to itself is the identity]
We prove that $F \circ G$ is homotopic to $\operatorname{id}_R$. Let $r:R$ be arbitrary. By Sigma elimination on $r$, it is enough to consider $r=(p,z)$, where
\begin{align*}
p:\Sigma_{x:A}B(x)
\end{align*}
and
\begin{align*}
z:C(\pi_1(p),\pi_2(p)).
\end{align*}
By the Sigma-type elimination principle [citetheorem:9631] applied to the pair $p$, it is enough to prove the claim when $p=(x,y)$ for $x:A$ and $y:B(x)$. In that case, by the Sigma beta rules [citetheorem:9629], the element $z$ has type $C(x,y)$, and
\begin{align*}
F(G((x,y),z)) = F(x,(y,z)).
\end{align*}
By the definition of $F$,
\begin{align*}
F(x,(y,z)) = ((x,y),z).
\end{align*}
Hence, for every $r:R$, there is a path
\begin{align*}
\varepsilon_r : F(G(r)) = r.
\end{align*}
This argument uses Sigma elimination rather than judgmental Sigma eta; equivalently, one may use the propositional Sigma eta principle [citetheorem:9630] to identify $p$ with $(\pi_1(p),\pi_2(p))$.
[/step]
[step:Package the reassociation maps as an equivalence]
The data constructed above consist of functions
\begin{align*}
F : L \to R
\end{align*}
and
\begin{align*}
G : R \to L,
\end{align*}
together with homotopies
\begin{align*}
\eta : \prod_{\ell:L} G(F(\ell)) = \ell
\end{align*}
and
\begin{align*}
\varepsilon : \prod_{r:R} F(G(r)) = r.
\end{align*}
By the definition of equivalence of types as a map equipped with a two-sided inverse up to identity, $F$ is an equivalence. Substituting the definitions of $L$ and $R$, we obtain
\begin{align*}
\Sigma_{x:A}\Sigma_{y:B(x)}C(x,y) \simeq \Sigma_{p:\Sigma_{x:A}B(x)} C(\pi_1(p),\pi_2(p)).
\end{align*}
This is the desired associativity equivalence for dependent Sigma types.
[/step]
