2.7 Ξ£-types

Let A be a type and B:A→𝒰 a type family. Recall that the Ξ£-type, or dependent pair type, βˆ‘(x:A)B⁒(x) is a generalizationPlanetmathPlanetmath of the cartesian productMathworldPlanetmath type. Thus, we expect its higher groupoidPlanetmathPlanetmathPlanetmathPlanetmath structureMathworldPlanetmath to also be a generalization of the previous sectionPlanetmathPlanetmath. 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β€² in βˆ‘(x:A)P⁒(x). Then we get 𝗉𝗋1(p):𝗉𝗋1(w)=𝗉𝗋1(wβ€²). However, we cannot directly ask whether 𝗉𝗋2⁒(w) is identical to 𝗉𝗋2⁒(wβ€²) since they don’t have to be in the same type. But we can transport 𝗉𝗋2⁒(w) along the path 𝗉𝗋1(p), and this does give us an element of the same type as 𝗉𝗋2⁒(wβ€²). By path inductionMathworldPlanetmath, we do in fact obtain a path 𝗉𝗋1(p)*(𝗉𝗋2(w))=𝗉𝗋2(wβ€²).

Recall from the discussion preceding Lemma 2.3.4 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem3) that 𝗉𝗋1(p)*(𝗉𝗋2(w))=𝗉𝗋2(wβ€²) can be regarded as the type of paths from 𝗉𝗋2⁒(w) to 𝗉𝗋2⁒(wβ€²) which lie over the path 𝗉𝗋1(p) in A. Thus, we are saying that a path w=wβ€² in the total space determines (and is determined by) a path p:𝗉𝗋1⁒(w)=𝗉𝗋1⁒(wβ€²) in A together with a path from 𝗉𝗋2⁒(w) to 𝗉𝗋2⁒(wβ€²) lying over p, which seems sensible.

Remark 2.7.1.

Note that if we have x:A and u,v:P⁒(x) such that (x,u)=(x,v), it does not follow that u=v. All we can conclude is that there exists p:x=x such that p*(u)=v. This is a well-known source of confusion for newcomers to type theoryPlanetmathPlanetmath, but it makes sense from a topological viewpoint: the existence of a path (x,u)=(x,v) 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=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:Aβ†’U is a type family over a type A and let w,wβ€²:βˆ‘(x:A)P⁒(x). Then there is an equivalence


We define for any w,wβ€²:βˆ‘(x:A)P⁒(x), a function


by path induction, with


We want to show that f is an equivalence.

In the reverse direction, we define


by first inducting on w and wβ€², which splits them into (w1,w2) and (w1β€²,w2β€²) respectively, so it suffices to show


Next, given a pair βˆ‘(p:w1=w1β€²)p*(w2)=w2β€², we can use Ξ£-induction to get p:w1=w1β€² and q:p*(w2)=w2β€². Inducting on p, we have q:𝗋𝖾𝖿𝗅*(w2)=w2β€², and it suffices to show (w1,w2)=(w1,w2β€²). But 𝗋𝖾𝖿𝗅*(w2)≑w2, so inducting on q reduces to the goal to (w1,w2)=(w1,w2), which we can prove with 𝗋𝖾𝖿𝗅(w1,w2).

Next we show that f∘g is the identityPlanetmathPlanetmathPlanetmath for all w, wβ€² and r, where r has type


First, we break apart the pairs w, wβ€², and r by pair induction, as in the definition of g, and then use two path inductions to reduce both components of r to 𝗋𝖾𝖿𝗅. Then it suffices to show that f⁒(g⁒(𝗋𝖾𝖿𝗅,𝗋𝖾𝖿𝗅))=𝗋𝖾𝖿𝗅, which is true by definition.

Similarly, to show that g∘f is the identity for all w, wβ€², and p:w=wβ€², we can do path induction on p, and then induction to split w, at which point it suffices to show that g⁒(f⁒(𝗋𝖾𝖿𝗅(w1,w2)))=𝗋𝖾𝖿𝗅(w1,w2), which is true by definition.

Thus, f has a quasi-inversePlanetmathPlanetmath, 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:βˆ‘(x:A)P⁒(x), we have z=(pr1⁒(z),pr2⁒(z)).


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

Note that the lifted path 𝗅𝗂𝖿𝗍⁒(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


This appears in the statement of action of transport on Ξ£-types, which is also a generalization of the action for binary cartesian products:

Theorem 2.7.4.

Suppose we have type families


Then we can construct the type family over A defined by


For any path p:x=y and any (u,z):βˆ‘(u:P(x))Q⁒(x,u) we have


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 reflexivityMathworldPlanetmath, inversesMathworldPlanetmathPlanetmathPlanetmath, and composition of Ξ£-types componentwise.

Title 2.7 Ξ£-types