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 of the second component of a pair to vary depending on the choice of the first component. This is called a dependent pair type, or $\Sigma$ -type, because in set theory it corresponds to an indexed sum (in the sense of coproduct or disjoint union) over a given type.

Given a type $A:\mathcal{U}$ and a family $B:A\to\mathcal{U}$ , the dependent pair type is written as $\textstyle\sum_{(x:A)}B(x):\mathcal{U}$ . Alternative notations are

\textstyle\sum_{(x:A)}B(x)\hskip 56.905512pt\sum_{(x:A)}\,B(x)\hskip 56.905512% pt\sum({\textstyle x:A}),\ B(x).

Like other binding constructs such as $\lambda$ -abstractions and $\Pi$ s, $\Sigma$ s automatically scope over the rest of the expression unless delimited, so e.g. $\textstyle\sum_{(x:A)}B(x)\times C(x)$ means $\textstyle\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):\textstyle\sum_{(x:A)}B(x)$ given $a : A$ and $b:B(a)$ . If $B$ is constant, then the dependent pair type is the ordinary cartesian product type:

\Bigl{(}\textstyle\sum_{(x:A)}B\Bigr{)}\equiv(A\times B).

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

For instance, the recursion principle says that to define a non-dependent function out of a $\Sigma$ -type $f:(\textstyle\sum_{(x:A)}B(x))\to C$ , we provide a function $g:\textstyle\prod_{(x:A)}B(x)\to C$ , and then we can define $f$ via the defining equation

f((a,b))܃\!\!\equiv g(a)(b).

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

\mathsf{pr}_{1}:\Bigl{(}\textstyle\sum_{(x:A)}B(x)\Bigr{)}\to A.

by the defining equation

\mathsf{pr}_{1}((a,b))܃\!\!\equiv a.

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

\mathsf{pr}_{2}:\textstyle\prod_{(p:\textstyle\sum_{(x:A)}B(x))}B(\mathsf{pr}_% {1}(p)).

Thus we need the induction principle for $\Sigma$ -types (the “dependent eliminator”). This says that to construct a dependent function out of a $\Sigma$ -type into a family $C:(\textstyle\sum_{(x:A)}B(x))\to\mathcal{U}$ , we need a function

g:\textstyle\prod_{(a:A)}{b:B(a)}C((a,b)).

We can then derive a function

f:\textstyle\prod_{(p:\textstyle\sum_{(x:A)}B(x))}C(p)

with defining equation

f((a,b))܃\!\!\equiv g(a)(b).

Applying this with $C(p)܃\!\!\equiv B(\mathsf{pr}_{1}(p))$ , we can define $\mathsf{pr}_{2}:\textstyle\prod_{(p:\textstyle\sum_{(x:A)}B(x))}B(\mathsf{pr}_% {1}(p))$ with the obvious equation

\mathsf{pr}_{2}((a,b))܃\!\!\equiv b.

To convince ourselves that this is correct, we note that $B(\mathsf{pr}_{1}((a,b)))\equiv B(a)$ , using the defining equation for $\mathsf{pr}_{1}$ , and indeed $b:B(a)$ .

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

\mathsf{rec}_{\textstyle\sum_{(x:A)}B(x)}:\prod_{(C:\mathcal{U})}\,\Bigl{(}% \textstyle\prod_{(x:A)}B(x)\to C\Bigr{)}\to\Bigl{(}\textstyle\sum_{(x:A)}B(x)% \Bigr{)}\to C

with the defining equation

\mathsf{rec}_{\textstyle\sum_{(x:A)}B(x)}(C,g,(a,b))܃\!\!\equiv g(a)(b)

and the corresponding induction operator:

\mathsf{ind}_{\textstyle\sum_{(x:A)}B(x)}:\prod_{(C:(\textstyle\sum_{(x:A)}B(x% ))\to\mathcal{U})}\,\Bigl{(}\textstyle\prod_{(a:A)}{b:B(a)}C((a,b))\Bigr{)}\to% \prod_{(p:\textstyle\sum_{(x:A)}B(x))}\,C(p)

with the defining equation

\mathsf{ind}_{\textstyle\sum_{(x:A)}B(x)}(C,g,(a,b))܃\!\!\equiv g(a)(b).

As before, the recursor is the special case of induction when 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\mathcal{U}$ .

\mathsf{ac}:\Bigl{(}\textstyle\prod_{(x:A)}\textstyle\sum_{(y:B)}R(x,y)\Bigr{)% }\to\Bigl{(}\textstyle\sum_{(f:A\to B)}\textstyle\prod_{(x:A)}R(x,f(x))\Bigr{)}

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 $\mathsf{ac}$ 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:

\mathsf{ac}(g)܃\!\!\equiv\Bigl{(}{\lambda}x{.\,}\mathsf{pr}_{1}(g(x)),\,{% \lambda}x{.\,}\mathsf{pr}_{2}(g(x))\Bigr{)}.

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

	$\displaystyle{\lambda}x{.\,}\mathsf{pr}_{1}(g(x))$	$\displaystyle:A\to B,$
	$\displaystyle{\lambda}x{.\,}\mathsf{pr}_{2}(g(x))$	$\displaystyle:\textstyle\prod_{(x:A)}R(x,\mathsf{pr}_{1}(g(x))).$

Moreover, the type $\textstyle\prod_{(x:A)}R(x,\mathsf{pr}_{1}(g(x)))$ is the result of substituting the function ${\lambda}x{.\,}\mathsf{pr}_{1}(g(x))$ for $f$ in the family being summed over in the codomain of $\mathsf{ac}$ :

\textstyle\prod_{(x:A)}R(x,\mathsf{pr}_{1}(g(x)))\equiv\Bigl{(}{\lambda}f{.\,}% \textstyle\prod_{(x:A)}R(x,f(x))\Bigr{)}\big{(}{\lambda}x{.\,}\mathsf{pr}_{1}(% g(x))\big{)}.

Thus, we have

\Bigl{(}{\lambda}x{.\,}\mathsf{pr}_{1}(g(x)),\,{\lambda}x{.\,}\mathsf{pr}_{2}(% g(x))\Bigr{)}:\textstyle\sum_{(f:A\to B)}\textstyle\prod_{(x:A)}R(x,f(x))

as required.

If we read $\Pi$ as “for all” and $\Sigma$ as “there exists”, then the type of the function $\mathsf{ac}$ expresses: if for all $x : A$ there is a $y : B$ such that $R(x,y)$ , then there is a function $f:A\to B$ such that for all $x : A$ we have $R(x,f(x))$ . Since this sounds like a version of the axiom of choice, the function $\mathsf{ac}$ 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 \autorefsec: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:\mathcal{U}$ 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

\mathsf{Magma}܃\!\!\equiv\textstyle\sum_{(A:\mathcal{U})}(A\to A\to A).

Given a magma, we extract its underlying type (its “carrier”) with the first projection $\mathsf{pr}_{1}$ , and its operation with the second projection $\mathsf{pr}_{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

\mathsf{PointedMagma}܃\!\!\equiv\textstyle\sum_{(A:\mathcal{U})}(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 $\Sigma$ -types; see \autorefsec: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 $\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 $\mathsf{PointedMagma}$ are of the form $(A,(m,e))$ where $A:\mathcal{U}$ , $m:A\to A\to A$ , and $e : A$ . Because of the frequency with which iterated $\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)܃\!\!\equiv(x,(y,z))$ and $(x,y,z,w)܃\!\!\equiv(x,(y,(z,w)))$ , etc.

Title	1.6 Dependent pair types
Canonical name	16DependentPairTypes
Date of creation	2013-11-13 18:01:54
Last modified on	2013-11-13 18:01:54
Owner	PMBookProject (1000683)
Last modified by	rspuzio (6075)
Numerical id	22
Author	PMBookProject (6075)
Entry type	Definition
Classification	msc 03B15