2.7 $\mathrm{\Sigma }$-types

Let $A$ be a type and $B:A\to 𝒰$ a type family. Recall that the $\mathrm{\Sigma }$-type, or dependent pair type, ${\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 ${\sum }_{(x:A)}P(x)$. Then we get ${\mathrm{𝗉𝗋}}_1\left(p\right):{\mathrm{𝗉𝗋}}_1(w)={\mathrm{𝗉𝗋}}_1(w^{\prime })$. However, we cannot directly ask whether ${\mathrm{𝗉𝗋}}_2(w)$ is identical to ${\mathrm{𝗉𝗋}}_2(w^{\prime })$ since they don’t have to be in the same type. But we can transport ${\mathrm{𝗉𝗋}}_2(w)$ along the path ${\mathrm{𝗉𝗋}}_1\left(p\right)$, and this does give us an element of the same type as ${\mathrm{𝗉𝗋}}_2(w^{\prime })$. By path induction, we do in fact obtain a path ${\mathrm{𝗉𝗋}}_1{\left(p\right)}_{*}\left({\mathrm{𝗉𝗋}}_2(w)\right)={\mathrm{𝗉𝗋}}_2(w^{\prime })$.

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

Remark 2.7.1.

Note that if we have $x\mathrm{:}A$ and $u\mathrm{,}v\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}$ such that $\mathrm{(}x\mathrm{,}u\mathrm{)}\mathrm{=}\mathrm{(}x\mathrm{,}v\mathrm{)}$, it does not follow that $u\mathrm{=}v$. All we can conclude is that there exists $p\mathrm{:}x\mathrm{=}x$ such that $p_{\mathrm{*}}\mathrm{\left(}u\mathrm{\right)}\mathrm{=}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 $\mathrm{(}x\mathrm{,}u\mathrm{)}\mathrm{=}\mathrm{(}x\mathrm{,}v\mathrm{)}$ 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\mathrm{=}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\mathrm{:}A\mathrm{\to }\mathrm{U}$ is a type family over a type $A$ and let $w\mathrm{,}{w}^{\mathrm{\prime }}\mathrm{:}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$. Then there is an equivalence

$$(w=w^{\prime })\simeq \sum _{(p:{\mathrm{𝗉𝗋}}_1(w)={\mathrm{𝗉𝗋}}_1(w^{\prime }))}{p}_{*}\left({\mathrm{𝗉𝗋}}_2(w)\right)={\mathrm{𝗉𝗋}}_2(w^{\prime }).$$

Proof.

We define for any $w,w^{\prime }:{\sum }_{(x:A)}P(x)$, a function

$$f:(w=w^{\prime })\to \sum _{(p:{\mathrm{𝗉𝗋}}_1(w)={\mathrm{𝗉𝗋}}_1(w^{\prime }))}{p}_{*}\left({\mathrm{𝗉𝗋}}_2(w)\right)={\mathrm{𝗉𝗋}}_2(w^{\prime })$$

by path induction, with

$$f(w,w,{\mathrm{𝗋𝖾𝖿𝗅}}_w):\equiv ({\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_1(w)},{\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_2(w)}).$$

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

In the reverse direction, we define

$$g:\prod _{w,w^{\prime }:{\sum }_{(x:A)}P(x)}(\sum _{p:{\mathrm{𝗉𝗋}}_1(w)={\mathrm{𝗉𝗋}}_1(w^{\prime })}{p}_{*}\left({\mathrm{𝗉𝗋}}_2(w)\right)={\mathrm{𝗉𝗋}}_2(w^{\prime }))\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

$$(\sum _{p:w_1=w_1^{\prime }}{p}_{*}\left(w_2\right)=w_2^{\prime })\to ((w_1,w_2)=(w_1^{\prime },w_2^{\prime })).$$

Next, given a pair ${\sum }_{(p:w_1=w_1^{\prime })}{p}_{*}\left(w_2\right)=w_2^{\prime }$, we can use $\mathrm{\Sigma }$-induction to get $p:w_1=w_1^{\prime }$ and $q:p_{*}\left(w_2\right)=w_2^{\prime }$. Inducting on $p$, we have $q:{\mathrm{𝗋𝖾𝖿𝗅}}_{*}\left(w_2\right)=w_2^{\prime }$, and it suffices to show $(w_1,w_2)=(w_1,w_2^{\prime })$. But ${\mathrm{𝗋𝖾𝖿𝗅}}_{*}\left(w_2\right)\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 ${\mathrm{𝗋𝖾𝖿𝗅}}_{(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:{\mathrm{𝗉𝗋}}_1(w)={\mathrm{𝗉𝗋}}_1(w^{\prime }))}(p_{*}\left({\mathrm{𝗉𝗋}}_2(w)\right)={\mathrm{𝗉𝗋}}_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 $\mathrm{𝗋𝖾𝖿𝗅}$. Then it suffices to show that $f(g(\mathrm{𝗋𝖾𝖿𝗅},\mathrm{𝗋𝖾𝖿𝗅}))=\mathrm{𝗋𝖾𝖿𝗅}$, 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({\mathrm{𝗋𝖾𝖿𝗅}}_{(w_1,w_2)}))={\mathrm{𝗋𝖾𝖿𝗅}}_{(w_1,w_2)}$, which is true by definition.

Thus, $f$ has a quasi-inverse, and is therefore an equivalence. ∎

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\mathrm{:}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$, we have $z\mathrm{=}\mathrm{(}{\mathrm{pr}}_{\mathrm{1}}\mathit{}\mathrm{(}z\mathrm{)}\mathrm{,}{\mathrm{pr}}_{\mathrm{2}}\mathit{}\mathrm{(}z\mathrm{)}\mathrm{)}$.

Proof.

We have ${\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_1(z)}:{\mathrm{𝗉𝗋}}_1(z)={\mathrm{𝗉𝗋}}_1({\mathrm{𝗉𝗋}}_1(z),{\mathrm{𝗉𝗋}}_2(z))$, so by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) it will suffice to exhibit a path ${({\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_1(z)})}_{*}\left({\mathrm{𝗉𝗋}}_2(z)\right)={\mathrm{𝗉𝗋}}_2({\mathrm{𝗉𝗋}}_1(z),{\mathrm{𝗉𝗋}}_2(z))$. But both sides are judgmentally equal to ${\mathrm{𝗉𝗋}}_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 (${\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}$), the forward direction as elimination forms (${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}$ and ${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}$), and the equivalence as giving a propositional computation rule and uniqueness principle for these.

Note that the lifted path $\mathrm{𝗅𝗂𝖿𝗍}(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

$${\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(p,{\mathrm{𝗋𝖾𝖿𝗅}}_{p_{*}\left(u\right)}):(x,u)=(y,p_{*}\left(u\right)).$$

This appears in the statement of action of transport on $\mathrm{\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 𝒰\mathit{\hspace{1em}\hspace{1em}}\text{𝑎𝑛𝑑}\mathit{\hspace{1em}\hspace{1em}}Q:\left(\sum _{x:A}P(x)\right)\to 𝒰.$$

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

$$x\mapsto \sum _{u:P(x)}Q(x,u).$$

For any path $p\mathrm{:}x\mathrm{=}y$ and any $\mathrm{(}u\mathrm{,}z\mathrm{)}\mathrm{:}{\mathrm{\sum }}_{\mathrm{(}u\mathrm{:}P\mathrm{(}x\mathrm{)}\mathrm{)}}Q\mathit{}\mathrm{(}x\mathrm{,}u\mathrm{)}$ we have

$$p_{*}(u,z)=(p_{*}\left(u\right),{\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}{(p,{\mathrm{𝗋𝖾𝖿𝗅}}_{p_{*}\left(u\right)})}_{*}\left(z\right)).$$

Proof.

Immediate by path induction. ∎

We leave it to the reader to state and prove a generalization of Theorem 2.6.5 (http://planetmath.org/26cartesianproducttypes#Thmprethm3) (see http://planetmath.org/node/87638Exercise 2.7), and to characterize the reflexivity, inverses, and composition of $\mathrm{\Sigma }$-types componentwise.

Title	2.7 $\mathrm{\Sigma }$-types