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 -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 and a family , the dependent pair type is written as . Alternative notations are
Like other binding constructs such as -abstractions and s, s automatically scope over the rest of the expression unless delimited, so e.g. means .
For instance, we can derive the first projection from a -type:
by the defining equation
However, since the type of the second component of a pair is , the second projection must be a dependent function, whose type involves the first projection function:
Thus we need the induction principle for -types (the “dependent eliminator”). This says that to construct a dependent function out of a -type into a family , we need a function
We can then derive a function
with defining equation
Applying this with , we can define with the obvious equation
To convince ourselves that this is correct, we note that , using the defining equation for , and indeed .
We can package the recursion and induction principles into the recursor for :
with the defining equation
and the corresponding induction operator:
with the defining equation
As before, the recursor is the special case of induction when the family is constant.
As a further example, consider the following principle, where and are types and .
We may regard as a “proof-relevant relation” between and , with the type of witnesses for relatedness of and . Then says intuitively that if we have a dependent function assigning to every a dependent pair where and , then we have a function and a dependent function assigning to every a witness that . Our intuition tells us that we can just split up the values of into their components. Indeed, using the projections we have just defined, we can define:
To verify that this is well-typed, note that if , we have
Moreover, the type is the result of substituting the function for in the family being summed over in the codomain of :
Thus, we have
If we read as “for all” and as “there exists”, then the type of the function expresses: if for all there is a such that , then there is a function such that for all we have . Since this sounds like a version of the axiom of choice, the function 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 together with a binary operation . The precise meaning of the phrase “together with” (and the synonymous “equipped with”) is that “a magma” is a pair consisting of a type and an operation . Since the type of the second component of this pair depends on its first component , such pairs belong to a dependent pair type. Thus, the definition “a magma is a type together with a binary operation ” should be read as defining the type of magmas to be
Given a magma, we extract its underlying type (its “carrier”) with the first projection , and its operation with the second projection . 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 equipped with a basepoint ) is
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 -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 -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 with its operation .
Note that the canonical elements of are of the form where , , and . Because of the frequency with which iterated -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 and , etc.
|Title||1.6 Dependent pair types|
|Date of creation||2013-11-13 18:01:54|
|Last modified on||2013-11-13 18:01:54|
|Last modified by||rspuzio (6075)|