# 2.7 $\Sigma$-types

Let $A$ be a type and $B:A\to\mathcal{U}$ a type family. Recall that the $\Sigma$-type, or dependent pair type, $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)$ is a generalization  of the cartesian product  type. Thus, we expect its higher groupoid    structure  to also be a generalization of the previous section  . In particular, its paths should be pairs of paths, but it takes a little thought to give the correct types of these paths.

Suppose that we have a path $p:w=w^{\prime}$ in $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$. Then we get ${\mathsf{pr}_{1}}\mathopen{}\left({p}\right)\mathclose{}:\mathsf{pr}_{1}(w)=% \mathsf{pr}_{1}(w^{\prime})$. However, we cannot directly ask whether $\mathsf{pr}_{2}(w)$ is identical to $\mathsf{pr}_{2}(w^{\prime})$ since they don’t have to be in the same type. But we can transport $\mathsf{pr}_{2}(w)$ along the path ${\mathsf{pr}_{1}}\mathopen{}\left({p}\right)\mathclose{}$, and this does give us an element of the same type as $\mathsf{pr}_{2}(w^{\prime})$. By path induction  , we do in fact obtain a path ${{\mathsf{pr}_{1}}\mathopen{}\left({p}\right)\mathclose{}}_{*}\mathopen{}\left% ({\mathsf{pr}_{2}(w)}\right)\mathclose{}=\mathsf{pr}_{2}(w^{\prime})$.

Recall from the discussion preceding Lemma 2.3.4 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem3) that ${{\mathsf{pr}_{1}}\mathopen{}\left({p}\right)\mathclose{}}_{*}\mathopen{}\left% ({\mathsf{pr}_{2}(w)}\right)\mathclose{}=\mathsf{pr}_{2}(w^{\prime})$ can be regarded as the type of paths from $\mathsf{pr}_{2}(w)$ to $\mathsf{pr}_{2}(w^{\prime})$ which lie over the path ${\mathsf{pr}_{1}}\mathopen{}\left({p}\right)\mathclose{}$ in $A$. Thus, we are saying that a path $w=w^{\prime}$ in the total space determines (and is determined by) a path $p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime})$ in $A$ together with a path from $\mathsf{pr}_{2}(w)$ to $\mathsf{pr}_{2}(w^{\prime})$ lying over $p$, which seems sensible.

###### Remark 2.7.1.

Note that if we have $x:A$ and $u,v:P(x)$ such that $(x,u)=(x,v)$, it does not follow that $u=v$. All we can conclude is that there exists $p:x=x$ such that ${p}_{*}\mathopen{}\left({u}\right)\mathclose{}=v$. This is a well-known source of confusion for newcomers to type theory  , but it makes sense from a topological viewpoint: the existence of a path $(x,u)=(x,v)$ in the total space of a fibration between two points that happen to lie in the same fiber does not imply the existence of a path $u=v$ lying entirely within that fiber.

The next theorem states that we can also reverse this process. Since it is a direct generalization of Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), we will be more concise.

###### Theorem 2.7.2.

Suppose that $P:A\to\mathcal{U}$ is a type family over a type $A$ and let $w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$. Then there is an equivalence

 $(w=w^{\prime})\;\simeq\;\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}% ))}\,{p}_{*}\mathopen{}\left({\mathsf{pr}_{2}(w)}\right)\mathclose{}=\mathsf{% pr}_{2}(w^{\prime}).$
###### Proof.

We define for any $w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$, a function

 $f:(w=w^{\prime})\to\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}\,% {p}_{*}\mathopen{}\left({\mathsf{pr}_{2}(w)}\right)\mathclose{}=\mathsf{pr}_{2% }(w^{\prime})$

by path induction, with

 $f(w,w,\mathsf{refl}_{w}):\!\!\equiv(\mathsf{refl}_{\mathsf{pr}_{1}(w)},\mathsf% {refl}_{\mathsf{pr}_{2}(w)}).$

We want to show that $f$ is an equivalence.

In the reverse direction, we define

 $g:\mathchoice{\prod_{w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x)}\,}{\mathchoice{{\textstyle\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:% A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)% }}{\sum_{(x:A)}}}P(x))}}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x))}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}}{\mathchoice{{\textstyle\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:% A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)% }}{\sum_{(x:A)}}}P(x))}}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x))}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}}{\mathchoice{{\textstyle\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:% A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)% }}{\sum_{(x:A)}}}P(x))}}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x))}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}{\prod_{(w,w^{\prime}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}}\Bigl{(}\mathchoice{\sum_{p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^% {\prime})}\,}{\mathchoice{{\textstyle\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{% 1}(w^{\prime}))}}}{\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}{% \sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}{\sum_{(p:\mathsf{pr% }_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}}{\mathchoice{{\textstyle\sum_{(p:% \mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}}{\sum_{(p:\mathsf{pr}_{1}(w)% =\mathsf{pr}_{1}(w^{\prime}))}}{\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^% {\prime}))}}{\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}}{% \mathchoice{{\textstyle\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime})% )}}}{\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}{\sum_{(p:% \mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}}{\sum_{(p:\mathsf{pr}_{1}(w)=% \mathsf{pr}_{1}(w^{\prime}))}}}{p}_{*}\mathopen{}\left({\mathsf{pr}_{2}(w)}% \right)\mathclose{}=\mathsf{pr}_{2}(w^{\prime})\Bigr{)}\to(w=w^{\prime})$

by first inducting on $w$ and $w^{\prime}$, which splits them into $(w_{1},w_{2})$ and $(w_{1}^{\prime},w_{2}^{\prime})$ respectively, so it suffices to show

 $\Bigl{(}\mathchoice{\sum_{p:w_{1}=w_{1}^{\prime}}\,}{\mathchoice{{\textstyle% \sum_{(p:w_{1}=w_{1}^{\prime})}}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}{\sum_{(p:w_% {1}=w_{1}^{\prime})}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}}{\mathchoice{{% \textstyle\sum_{(p:w_{1}=w_{1}^{\prime})}}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}{% \sum_{(p:w_{1}=w_{1}^{\prime})}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}}{\mathchoice% {{\textstyle\sum_{(p:w_{1}=w_{1}^{\prime})}}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}% {\sum_{(p:w_{1}=w_{1}^{\prime})}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}}{p}_{*}% \mathopen{}\left({w_{2}}\right)\mathclose{}=w_{2}^{\prime}\Bigr{)}\to((w_{1},w% _{2})=(w_{1}^{\prime},w_{2}^{\prime})).$

Next, given a pair $\mathchoice{\sum_{p:w_{1}=w_{1}^{\prime}}\,}{\mathchoice{{\textstyle\sum_{(p:w% _{1}=w_{1}^{\prime})}}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}{\sum_{(p:w_{1}=w_{1}^% {\prime})}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}}{\mathchoice{{\textstyle\sum_{(p:% w_{1}=w_{1}^{\prime})}}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}{\sum_{(p:w_{1}=w_{1}% ^{\prime})}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}}{\mathchoice{{\textstyle\sum_{(p% :w_{1}=w_{1}^{\prime})}}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}{\sum_{(p:w_{1}=w_{1% }^{\prime})}}{\sum_{(p:w_{1}=w_{1}^{\prime})}}}{p}_{*}\mathopen{}\left({w_{2}}% \right)\mathclose{}=w_{2}^{\prime}$, we can use $\Sigma$-induction to get $p:w_{1}=w_{1}^{\prime}$ and $q:{p}_{*}\mathopen{}\left({w_{2}}\right)\mathclose{}=w_{2}^{\prime}$. Inducting on $p$, we have $q:{\mathsf{refl}}_{*}\mathopen{}\left({w_{2}}\right)\mathclose{}=w_{2}^{\prime}$, and it suffices to show $(w_{1},w_{2})=(w_{1},w_{2}^{\prime})$. But ${\mathsf{refl}}_{*}\mathopen{}\left({w_{2}}\right)\mathclose{}\equiv w_{2}$, so inducting on $q$ reduces to the goal to $(w_{1},w_{2})=(w_{1},w_{2})$, which we can prove with $\mathsf{refl}_{(w_{1},w_{2})}$.

Next we show that $f\circ g$ is the identity   for all $w$, $w^{\prime}$ and $r$, where $r$ has type

 $\sum_{(p:\mathsf{pr}_{1}(w)=\mathsf{pr}_{1}(w^{\prime}))}\,({p}_{*}\mathopen{}% \left({\mathsf{pr}_{2}(w)}\right)\mathclose{}=\mathsf{pr}_{2}(w^{\prime})).$

First, we break apart the pairs $w$, $w^{\prime}$, and $r$ by pair induction, as in the definition of $g$, and then use two path inductions to reduce both components of $r$ to $\mathsf{refl}$. Then it suffices to show that $f(g(\mathsf{refl},\mathsf{refl}))=\mathsf{refl}$, which is true by definition.

Similarly, to show that $g\circ f$ is the identity for all $w$, $w^{\prime}$, and $p:w=w^{\prime}$, we can do path induction on $p$, and then induction to split $w$, at which point it suffices to show that $g(f(\mathsf{refl}_{(w_{1},w_{2})}))=\mathsf{refl}_{(w_{1},w_{2})}$, which is true by definition.

As we did in the case of cartesian products, we can deduce a propositional uniqueness principle as a special case.

###### Corollary 2.7.3.

For $z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}% }{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:% A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{% (x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$, we have $z=(\mathsf{pr}_{1}(z),\mathsf{pr}_{2}(z))$.

###### Proof.

We have $\mathsf{refl}_{\mathsf{pr}_{1}(z)}:\mathsf{pr}_{1}(z)=\mathsf{pr}_{1}(\mathsf{% pr}_{1}(z),\mathsf{pr}_{2}(z))$, so by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) it will suffice to exhibit a path ${(\mathsf{refl}_{\mathsf{pr}_{1}(z)})}_{*}\mathopen{}\left({\mathsf{pr}_{2}(z)% }\right)\mathclose{}=\mathsf{pr}_{2}(\mathsf{pr}_{1}(z),\mathsf{pr}_{2}(z))$. But both sides are judgmentally equal to $\mathsf{pr}_{2}(z)$. ∎

Like with binary cartesian products, we can think of the backward direction of Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) as an introduction form ($\mathsf{pair}^{\mathord{=}}$), the forward direction as elimination forms ($\mathsf{ap}_{\mathsf{pr}_{1}}$ and $\mathsf{ap}_{\mathsf{pr}_{2}}$), and the equivalence as giving a propositional computation rule and uniqueness principle for these.

Note that the lifted path $\mathsf{lift}(u,p)$ of $p:x=y$ at $u:P(x)$ defined in Lemma 2.3.2 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem2) may be identified with the special case of the introduction form

 $\mathsf{pair}^{\mathord{=}}(p,\mathsf{refl}_{{p}_{*}\mathopen{}\left({u}\right% )\mathclose{}}):(x,u)=(y,{p}_{*}\mathopen{}\left({u}\right)\mathclose{}).$

This appears in the statement of action of transport on $\Sigma$-types, which is also a generalization of the action for binary cartesian products:

###### Theorem 2.7.4.

Suppose we have type families

 $P:A\to\mathcal{U}\qquad\text{and}\qquad Q:\Bigl{(}\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x)\Bigr{)}\to\mathcal{U}.$

Then we can construct the type family over $A$ defined by

 $x\mapsto\mathchoice{\sum_{u:P(x)}\,}{\mathchoice{{\textstyle\sum_{(u:P(x))}}}{% \sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}}{\mathchoice{{\textstyle% \sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}}{% \mathchoice{{\textstyle\sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{% \sum_{(u:P(x))}}}Q(x,u).$

For any path $p:x=y$ and any $(u,z):\mathchoice{\sum_{u:P(x)}\,}{\mathchoice{{\textstyle\sum_{(u:P(x))}}}{% \sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}}{\mathchoice{{\textstyle% \sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}}{% \mathchoice{{\textstyle\sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{% \sum_{(u:P(x))}}}Q(x,u)$ we have

 ${p}_{*}\mathopen{}\left({u,z}\right)\mathclose{}=\big{(}{p}_{*}\mathopen{}% \left({u}\right)\mathclose{},\,{\mathsf{pair}^{\mathord{=}}(p,\mathsf{refl}_{{% p}_{*}\mathopen{}\left({u}\right)\mathclose{}})}_{*}\mathopen{}\left({z}\right% )\mathclose{}\big{)}.$
###### Proof.

Immediate by path induction. ∎

 Title 2.7 $\Sigma$-types \metatable