1.6 Dependent pair types

Just as we generalized function types (§1.2 (http://planetmath.org/12functiontypes)) to dependent function types (§1.4 (http://planetmath.org/14dependentfunctiontypes)), it is often useful to generalize the product types from §1.5 (http://planetmath.org/15producttypes) to allow the type ofthe second component of a pair to vary depending on the choice of the firstcomponent. This is called a dependent pair type, or $\mathrm{\Sigma }$-type, because in set theory itcorresponds to an indexed sum (in the sense of coproduct ordisjoint union) over a given type.

Given a type $A:𝒰$ and a family $B:A\to 𝒰$, the dependentpair type is written as ${\sum }_{(x:A)}B(x):𝒰$.Alternative notations are

$${\sum }_{(x:A)}B(x)\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em} }{\sum }_{(x:A)}B(x)\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em} }\sum (x:A),B(x).$$

Like other binding constructs such as $\lambda$-abstractions and $\mathrm{\Pi }$s, $\mathrm{\Sigma }$s automatically scope over the rest of the expression unless delimited, so e.g. ${\sum }_{(x:A)}B(x)\times C(x)$ means ${\sum }_{(x:A)}(B(x)\times C(x))$.

The way to construct elements of a dependent pair type is by pairing: we have$(a,b):{\sum }_{(x:A)}B(x)$ given $a:A$ and $b:B(a)$.If $B$ is constant, then the dependent pair type is theordinary cartesian product type:

$$\left({\sum }_{(x:A)}B\right)\equiv (A\times B).$$

All the constructions on $\mathrm{\Sigma }$-types arise as straightforward generalizations of the ones for product types, with dependent functions often replacing non-dependent ones.

For instance, the recursion principlesays that to define a non-dependent function out of a $\mathrm{\Sigma }$-type$f:({\sum }_{(x:A)}B(x))\to C$, we provide a function$g:{\prod }_{(x:A)}B(x)\to C$, and then we can define $f$ via the definingequation

$$f((a,b))Ü\mathrm{ƒ}\equiv g(a)(b).$$

For instance, we can derive the first projection from a $\mathrm{\Sigma }$-type:

$${\mathrm{𝗉𝗋}}_1:\left({\sum }_{(x:A)}B(x)\right)\to A.$$

by the defining equation

$${\mathrm{𝗉𝗋}}_1((a,b))Ü\mathrm{ƒ}\equiv a.$$

However, since the type of the second component of a pair$(a,b):{\sum }_{(x:A)}B(x)$is $B(a)$, the second projection must be a dependent function, whose type involves the first projection function:

$${\mathrm{𝗉𝗋}}_2:{\prod }_{(p:{\sum }_{(x:A)}B\left(x\right))}B({\mathrm{𝗉𝗋}}_1(p)).$$

Thus we need the induction principlefor $\mathrm{\Sigma }$-types (the “dependent eliminator”).This says that to construct a dependent function out of a $\mathrm{\Sigma }$-type into a family $C:({\sum }_{(x:A)}B(x))\to 𝒰$, we need a function

$$g:{\prod }_{(a:A)}b:B(a)C((a,b)).$$

We can then derive a function

$$f:{\prod }_{(p:{\sum }_{(x:A)}B\left(x\right))}C(p)$$

with defining equation

$$f((a,b))Ü\mathrm{ƒ}\equiv g(a)(b).$$

Applying this with $C(p)Ü\mathrm{ƒ}\equiv B({\mathrm{𝗉𝗋}}_1(p))$, we can define${\mathrm{𝗉𝗋}}_2:{\prod }_{(p:{\sum }_{(x:A)}B\left(x\right))}B({\mathrm{𝗉𝗋}}_1(p))$with the obvious equation

$${\mathrm{𝗉𝗋}}_2((a,b))Ü\mathrm{ƒ}\equiv b.$$

To convince ourselves that this is correct, we note that $B({\mathrm{𝗉𝗋}}_1((a,b)))\equiv B(a)$, using the defining equation for ${\mathrm{𝗉𝗋}}_1$, andindeed $b:B(a)$.

We can package the recursion and induction principles into the recursor for $\mathrm{\Sigma }$:

$${\mathrm{𝗋𝖾𝖼}}_{{\sum }_{(x:A)}B\left(x\right)}:\prod _{(C:𝒰)}({\prod }_{(x:A)}B(x)\to C)\to \left({\sum }_{(x:A)}B(x)\right)\to C$$

with the defining equation

$${\mathrm{𝗋𝖾𝖼}}_{{\sum }_{(x:A)}B\left(x\right)}(C,g,(a,b))Ü\mathrm{ƒ}\equiv g(a)(b)$$

and the corresponding induction operator:

$${\mathrm{𝗂𝗇𝖽}}_{{\sum }_{(x:A)}B\left(x\right)}:\prod _{(C:({\sum }_{(x:A)}B\left(x\right))\to 𝒰)}({\prod }_{(a:A)}b:B(a)C((a,b)))\to {\prod }_{(p:{\sum }_{(x:A)}B\left(x\right))}C(p)$$

with the defining equation

$${\mathrm{𝗂𝗇𝖽}}_{{\sum }_{(x:A)}B\left(x\right)}(C,g,(a,b))Ü\mathrm{ƒ}\equiv g(a)(b).$$

As before, the recursor is the special case of inductionwhen the family $C$ is constant.

As a further example, consider the following principle, where $A$ and $B$ are types and $R:A\to B\to 𝒰$.

$$\mathrm{𝖺𝖼}:\left({\prod }_{(x:A)}{\sum }_{(y:B)}R(x,y)\right)\to \left({\sum }_{(f:A\to B)}{\prod }_{(x:A)}R(x,f(x))\right)$$

We may regard $R$ as a “proof-relevant relation”between $A$ and $B$, with $R(a,b)$ the type of witnesses for relatedness of $a:A$ and $b:B$.Then $\mathrm{𝖺𝖼}$ says intuitively that if we have a dependent function $g$ assigning to every $a:A$ a dependent pair $(b,r)$ where $b:B$ and $r:R(a,b)$, then we have a function $f:A\to B$ and a dependent function assigning to every $a:A$ a witness that $R(a,f(a))$.Our intuition tells us that we can just split up the values of $g$ into their components.Indeed, using the projections we have just defined, we can define:

$$\mathrm{𝖺𝖼}(g)Ü\mathrm{ƒ}\equiv (\lambda x.{\mathrm{𝗉𝗋}}_1(g(x)),\lambda x.{\mathrm{𝗉𝗋}}_2(g(x))).$$

To verify that this is well-typed, note that if $g:{\prod }_{(x:A)}{\sum }_{(y:B)}R(x,y)$, we have

$\lambda x.{\mathrm{𝗉𝗋}}_1(g(x))$$:A\to B,$

$\lambda x.{\mathrm{𝗉𝗋}}_2(g(x))$$:{\prod }_{(x:A)}R(x,{\mathrm{𝗉𝗋}}_1(g(x))).$

Moreover, the type ${\prod }_{(x:A)}R(x,{\mathrm{𝗉𝗋}}_1(g(x)))$ is the result of substituting the function $\lambda x.{\mathrm{𝗉𝗋}}_1(g(x))$ for $f$ in the family being summed over in the codomain of $\mathrm{𝖺𝖼}$:

$${\prod }_{(x:A)}R(x,{\mathrm{𝗉𝗋}}_1(g(x)))\equiv (\lambda f.{\prod }_{(x:A)}R(x,f(x)))(\lambda x.{\mathrm{𝗉𝗋}}_1(g(x))).$$

Thus, we have

$$(\lambda x.{\mathrm{𝗉𝗋}}_1(g(x)),\lambda x.{\mathrm{𝗉𝗋}}_2(g(x))):{\sum }_{(f:A\to B)}{\prod }_{(x:A)}R(x,f(x))$$

as required.

If we read $\mathrm{\Pi }$ as “for all” and $\mathrm{\Sigma }$ as “there exists”, then the type of the function $\mathrm{𝖺𝖼}$ expresses:if for all $x\mathrm{:}A$ there is a $y\mathrm{:}B$ such that $R\mathit{}\mathrm{(}x\mathrm{,}y\mathrm{)}$, then there is a function $f\mathrm{:}A\mathrm{\to }B$ such that for all $x\mathrm{:}A$ we have $R\mathit{}\mathrm{(}x\mathrm{,}f\mathit{}\mathrm{(}x\mathrm{)}\mathrm{)}$.Since this sounds like a version of the axiom of choice, the function $\mathrm{𝖺𝖼}$ has traditionally been called the type-theoretic axiom of choice, and as we have just shown, it can be proved directly from the rules of type theory, rather than having to be taken as an axiom.However, note that no choice is actually involved, since the choices have already been given to us in the premise: all we have to do is take it apart into two functions: one representing the choice and the other its correctness.In sec:axiom-choice we will give another formulation of an “axiom of choice” which is closer to the usual one.

Dependent pair types are often used to define types of mathematical structures, which commonly consist of several dependent pieces of data.To take a simple example, suppose we want to define a magma to be a type $A$ together with a binary operation $m:A\to A\to A$.The precise meaning of the phrase “together with” (and the synonymous “equipped with”) is that “a magma” is a pair $(A,m)$ consisting of a type $A:𝒰$ and an operation $m:A\to A\to A$.Since the type $A\to A\to A$ of the second component $m$ of this pair depends on its first component $A$, such pairs belong to a dependent pair type.Thus, the definition “a magma is a type $A$ together with a binary operation $m:A\to A\to A$” should be read as defining the type of magmas to be

$$\mathrm{𝖬𝖺𝗀𝗆𝖺}Ü\mathrm{ƒ}\equiv {\sum }_{(A:𝒰)}(A\to A\to A).$$

Given a magma, we extract its underlying type (its “carrier”) with the first projection ${\mathrm{𝗉𝗋}}_1$, and its operation with the second projection ${\mathrm{𝗉𝗋}}_2$.Of course, structures built from more than two pieces of data require iterated pair types, which may be only partially dependent; for instance the type of pointed magmas (magmas $(A,m)$ equipped with a basepoint $e:A$) is

$$\mathrm{𝖯𝗈𝗂𝗇𝗍𝖾𝖽𝖬𝖺𝗀𝗆𝖺}Ü\mathrm{ƒ}\equiv {\sum }_{(A:𝒰)}(A\to A\to A)\times A.$$

We generally also want to impose axioms on such a structure, e.g. to make a pointed magma into a monoid or a group.This can also be done using $\mathrm{\Sigma }$-types; see sec:pat.

In the rest of the book, we will sometimes make definitions of this sort explicit, but eventually we trust the reader to translate them from English into $\mathrm{\Sigma }$-types.We also generally follow the common mathematical practice of using the same letter for a structure of this sort and for its carrier (which amounts to leaving the appropriate projection function implicit in the notation): that is, we will speak of a magma $A$ with its operation $m:A\to A\to A$.

Note that the canonical elements of $\mathrm{𝖯𝗈𝗂𝗇𝗍𝖾𝖽𝖬𝖺𝗀𝗆𝖺}$ are of the form $(A,(m,e))$ where $A:𝒰$, $m:A\to A\to A$, and $e:A$.Because of the frequency with which iterated $\mathrm{\Sigma }$-types of this sort arise, we use the usual notation of ordered triples, quadruples and so on to stand for nested pairs (possibly dependent) associating to the right.That is, we have $(x,y,z)Ü\mathrm{ƒ}\equiv (x,(y,z))$ and $(x,y,z,w)Ü\mathrm{ƒ}\equiv (x,(y,(z,w)))$, etc.