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 componentPlanetmathPlanetmathPlanetmath 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 theoryMathworldPlanetmath it corresponds to an indexed sum (in the sense of coproduct or disjoint unionMathworldPlanetmath) over a given type.

Given a type A:𝒰 and a family B:A→𝒰, the dependent pair type is written as βˆ‘(x:A)B⁒(x):𝒰. Alternative notations are

βˆ‘(x:A)B(x)β€ƒβ€ƒβ€ƒβ€ƒβ€ƒβ€‚β€†βˆ‘(x:A)B(x)β€ƒβ€ƒβ€ƒβ€ƒβ€ƒβ€‚β€†βˆ‘(x:A),B(x).

Like other binding constructs such as Ξ»-abstractions and Ξ s, Ξ£s automatically scope over the rest of the expression unless delimited, so e.g.Β βˆ‘(x:A)B⁒(x)Γ—C⁒(x) means βˆ‘(x:A)(B⁒(x)Γ—C⁒(x)).

The way to construct elements of a dependent pair type is by pairing: we have (a,b):βˆ‘(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:

(βˆ‘(x:A)B)≑(AΓ—B).

All the constructions on Ξ£-types arise as straightforward generalizationsPlanetmathPlanetmath 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 Ξ£-type f:(βˆ‘(x:A)B⁒(x))β†’C, we provide a function g:∏(x:A)B⁒(x)β†’C, and then we can define f via the defining equation

f⁒((a,b))β’Γœβ’Βƒβ‰‘g⁒(a)⁒(b).

For instance, we can derive the first projectionPlanetmathPlanetmath from a Ξ£-type:

𝗉𝗋1:(βˆ‘(x:A)B⁒(x))β†’A.

by the defining equation

𝗉𝗋1⁒((a,b))β’Γœβ’Βƒβ‰‘a.

However, since the type of the second component of a pair (a,b):βˆ‘(x:A)B⁒(x) is B⁒(a), the second projection must be a dependent function, whose type involves the first projection function:

𝗉𝗋2:∏(p:βˆ‘(x:A)B(x))B⁒(𝗉𝗋1⁒(p)).

Thus we need the inductionMathworldPlanetmath principle for Ξ£-types (the β€œdependent eliminator”). This says that to construct a dependent function out of a Ξ£-type into a family C:(βˆ‘(x:A)B⁒(x))→𝒰, we need a function

g:∏(a:A)b:B⁒(a)⁒C⁒((a,b)).

We can then derive a function

f:∏(p:βˆ‘(x:A)B(x))C⁒(p)

with defining equation

f⁒((a,b))β’Γœβ’Βƒβ‰‘g⁒(a)⁒(b).

Applying this with C⁒(p)β’Γœβ’Βƒβ‰‘B⁒(𝗉𝗋1⁒(p)), we can define 𝗉𝗋2:∏(p:βˆ‘(x:A)B(x))B⁒(𝗉𝗋1⁒(p)) with the obvious equation

𝗉𝗋2⁒((a,b))β’Γœβ’Βƒβ‰‘b.

To convince ourselves that this is correct, we note that B⁒(𝗉𝗋1⁒((a,b)))≑B⁒(a), using the defining equation for 𝗉𝗋1, and indeed b:B⁒(a).

We can package the recursion and induction principles into the recursor for Ξ£:

π—‹π–Ύπ–Όβˆ‘(x:A)B⁒(x):∏(C:𝒰)(∏(x:A)B(x)β†’C)β†’(βˆ‘(x:A)B(x))β†’C

with the defining equation

π—‹π–Ύπ–Όβˆ‘(x:A)B⁒(x)⁒(C,g,(a,b))β’Γœβ’Βƒβ‰‘g⁒(a)⁒(b)

and the corresponding induction operator:

π—‚π—‡π–½βˆ‘(x:A)B⁒(x):∏(C:(βˆ‘(x:A)B(x))→𝒰)(∏(a:A)b:B(a)C((a,b)))β†’βˆ(p:βˆ‘(x:A)B(x))C(p)

with the defining equation

π—‚π—‡π–½βˆ‘(x:A)B⁒(x)⁒(C,g,(a,b))β’Γœβ’Βƒβ‰‘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β†’B→𝒰.

𝖺𝖼:(∏(x:A)βˆ‘(y:B)R⁒(x,y))β†’(βˆ‘(f:Aβ†’B)∏(x:A)R⁒(x,f⁒(x)))

We may regard R as a β€œproof-relevant relationMathworldPlanetmath” between A and B, with R⁒(a,b) the type of witnesses for relatedness of a:A and b:B. Then 𝖺𝖼 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β†’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:

𝖺𝖼(g)ΓœΒƒβ‰‘(Ξ»x.𝗉𝗋1(g(x)),Ξ»x.𝗉𝗋2(g(x))).

To verify that this is well-typed, note that if g:∏(x:A)βˆ‘(y:B)R⁒(x,y), we have

λ⁒x.𝗉𝗋1⁒(g⁒(x)) :Aβ†’B,
λ⁒x.𝗉𝗋2⁒(g⁒(x)) :∏(x:A)R⁒(x,𝗉𝗋1⁒(g⁒(x))).

Moreover, the type ∏(x:A)R⁒(x,𝗉𝗋1⁒(g⁒(x))) is the result of substituting the function λ⁒x.𝗉𝗋1⁒(g⁒(x)) for f in the family being summed over in the codomain of 𝖺𝖼:

∏(x:A)R(x,𝗉𝗋1(g(x)))≑(Ξ»f.∏(x:A)R(x,f(x)))(Ξ»x.𝗉𝗋1(g(x))).

Thus, we have

(Ξ»x.𝗉𝗋1(g(x)),Ξ»x.𝗉𝗋2(g(x))):βˆ‘(f:Aβ†’B)∏(x:A)R(x,f(x))

as required.

If we read Ξ  as β€œfor all” and Ξ£ as β€œthere exists”, then the type of the function 𝖺𝖼 expresses: if for all x:A there is a y:B such that R⁒(x,y), then there is a function f:Aβ†’B such that for all x:A we have R⁒(x,f⁒(x)). Since this sounds like a version of the axiom of choiceMathworldPlanetmath, 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 theoryPlanetmathPlanetmath, 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 premiseMathworldPlanetmath: 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 operationMathworldPlanetmath m:Aβ†’Aβ†’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 operationMathworldPlanetmath m:Aβ†’Aβ†’A. Since the type Aβ†’Aβ†’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β†’Aβ†’A” should be read as defining the type of magmas to be

π–¬π–Ίπ—€π—†π–ΊΓœΒƒβ‰‘βˆ‘(A:𝒰)(Aβ†’Aβ†’A).

Given a magma, we extract its underlying type (its β€œcarrier”) with the first projection 𝗉𝗋1, and its operation with the second projection 𝗉𝗋2. Of course, structuresMathworldPlanetmath 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

π–―π—ˆπ—‚π—‡π—π–Ύπ–½π–¬π–Ίπ—€π—†π–ΊΓœΒƒβ‰‘βˆ‘(A:𝒰)(Aβ†’Aβ†’A)Γ—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 Ξ£-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 translateMathworldPlanetmath 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 A with its operation m:A→A→A.

Note that the canonical elements of π–―π—ˆπ—‚π—‡π—π–Ύπ–½π–¬π–Ίπ—€π—†π–Ί are of the form (A,(m,e)) where A:𝒰, m:Aβ†’Aβ†’A, and e:A. 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 (x,y,z)β’Γœβ’Βƒβ‰‘(x,(y,z)) and (x,y,z,w)β’Γœβ’Βƒβ‰‘(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