[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*}[/step]

[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: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]