6.12 The flattening lemma


As we will see in http://planetmath.org/node/87582Chapter 8, amazing things happen when we combine higher inductive types with univalence. The principal way this comes about is that if W is a higher inductive type and 𝒰 is a type universePlanetmathPlanetmath, then we can define a type family P:W→𝒰 by using the recursion principle for W. When we come to the clauses of the recursion principle dealing with the path constructors of W, we will need to supply paths in 𝒰, and this is where univalence comes in.

For example, suppose we have a type X and a self-equivalence e:X≃X. Then we can define a type family P:π•Š1→𝒰 by using π•Š1-recursion:

P(π–»π–Ίπ—Œπ–Ύ):≑X  and  P(π—…π—ˆπ—ˆπ—‰):=π—Žπ–Ί(e).

The type X thus appears as the fiber P⁒(π–»π–Ίπ—Œπ–Ύ) of P over the basepoint. The self-equivalence e is a little more hidden in P, but the following lemma says that it can be extracted by transporting along π—…π—ˆπ—ˆπ—‰.

Lemma 6.12.1.

Given B:Aβ†’U and x,y:A, with a path p:x=y and an equivalence e:P⁒(x)≃P⁒(y) such that B(p)=ua(e), then for any u:P⁒(x) we have

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—B⁒(p,u) =e⁒(u).
Proof.

Applying Lemma 2.10.5 (http://planetmath.org/210universesandtheunivalenceaxiom#Thmprelem2), we have

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—B⁒(p,u) =π—‚π–½π—π—ˆπ–Ύπ—Šπ—(B(p))(u)
=π—‚π–½π—π—ˆπ–Ύπ—Šπ—β’(π—Žπ–Ίβ’(e))⁒(u)
=e⁒(u).∎

We have seen type families defined by recursion before: in Β§2.12 (http://planetmath.org/212coproducts),Β§2.13 (http://planetmath.org/213naturalnumbers) we used them to characterize the identity types of (ordinary) inductive types. In http://planetmath.org/node/87582Chapter 8, we will use similar ideas to calculate homotopy groups of higher inductive types.

In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we describe a general lemma about type families of this sort which will be useful later on. We call it the flattening lemma: it says that if P:W→𝒰 is defined recursively as above, then its total space βˆ‘(x:W)P⁒(x) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to a β€œflattened” higher inductive type, whose constructors may be deduced from those of W and the definition of P. From a category-theoretic point of view, βˆ‘(x:W)P⁒(x) is the β€œGrothendieck construction” of P, and this expresses its universal propertyMathworldPlanetmath as a β€œlax colimitMathworldPlanetmath”.

We prove here one general case of the flattening lemma, which directly implies many particular cases and suggests the method to prove others. Suppose we have A,B:𝒰 and f,g:Bβ†’A, and that the higher inductive type W is generated by

  • β€’

    𝖼:Aβ†’W and

  • β€’

    𝗉:∏(b:B)(𝖼(f(b))=W𝖼(g(b))).

Thus, W is the (homotopy) coequalizerMathworldPlanetmath of f and g. Using binary sums (coproductsMathworldPlanetmath) and dependent sums (Ξ£-types), a lot of interesting nonrecursive higher inductive types can be represented in this form. All point constructors have to be bundled in the type A and all path constructors in the type B. For instance:

  • β€’

    The circle π•Š1 can be represented by taking A:β‰‘πŸ and B:β‰‘πŸ, with f and g the identityPlanetmathPlanetmath.

  • β€’

    The pushout of j:Xβ†’Y and k:Xβ†’Z can be represented by taking A:≑Y+Z and B:≑X, with f:β‰‘π—‚π—‡π—…βˆ˜j and g:β‰‘π—‚π—‡π—‹βˆ˜k.

Now suppose in addition that

  • β€’

    C:A→𝒰 is a family of types over A, and

  • β€’

    D:∏(b:B)C⁒(f⁒(b))≃C⁒(g⁒(b)) is a family of equivalences over B.

Define a type family P:W→𝒰 inductively by

P⁒(𝖼⁒(a)) :≑C(a)
P(𝗉(b)) :=π—Žπ–Ίβ’(D⁒(b)).

Let W~ be the higher inductive type generated by

  • β€’

    𝖼~:∏(a:A)C⁒(a)β†’W~ and

  • β€’

    𝗉~:∏(b:B)∏(y:C(f(b)))(𝖼~(f(b),y)=W~𝖼~(g(b),D(b)(y))).

The flattening lemma is:

Lemma 6.12.2 (Flattening lemma).

In the above situation, we have

(βˆ‘x:WP⁒(x))≃W~.

As remarked above, this equivalence can be seen as expressing the universal property of βˆ‘(x:W)P⁒(x) as a β€œlax colimit” of P over W. It can also be seen as part of the stability and descent property of colimits, which characterizes higher toposes.

The proof of Lemma 6.12.2 (http://planetmath.org/612theflatteninglemma#Thmprelem2) occupies the rest of this section. It is somewhat technical and can be skipped on a first reading. But it is also a good example of β€œproof-relevant mathematics”, so we recommend it on a second reading.

The idea is to show that βˆ‘(x:W)P⁒(x) has the same universal property as W~. We begin by showing that it comes with analogues of the constructors 𝖼~ and 𝗉~.

Lemma 6.12.3.

There are functions

  • β€’

    𝖼~β€²:∏(a:A)C⁒(a)β†’βˆ‘(x:W)P⁒(x) and

  • β€’

    𝗉~β€²:∏(b:B)∏(y:C(f(b)))(𝖼~β€²(f(b),y)=βˆ‘(w:W)P⁒(w)𝖼~β€²(g(b),D(b)(y))).

Proof.

The first is easy; define 𝖼~β€²(a,x):≑(𝖼(a),x) and note that by definition P⁒(𝖼⁒(a))≑C⁒(a). For the second, suppose given b:B and y:C⁒(f⁒(b)); we must give an equality

(𝖼⁒(f⁒(b)),y)=(𝖼⁒(g⁒(b),D⁒(b)⁒(y))).

Since we have 𝗉⁒(b):f⁒(b)=g⁒(b), by equalities in Ξ£-types it suffices to give an equality 𝗉(b)*(y)=D(b)(y). But this follows from Lemma 6.12.1 (http://planetmath.org/612theflatteninglemma#Thmprelem1), using the definition of P. ∎

Now the following lemma says to define a section of a type family over βˆ‘(w:W)P⁒(w), it suffices to give analogous data as in the case of W~.

Lemma 6.12.4.

Suppose Q:(βˆ‘(x:W)P⁒(x))β†’U is a type family and that we have

  • β€’

    c:∏(a:A)∏(x:C(a))Q⁒(𝖼~′⁒(a,x)) and

  • β€’

    p:∏(b:B)∏(y:C(f(b)))(𝗉~β€²(b,y)*(c(f(b),y))=c(g(b),D(b)(y))).

Then there exists f:∏(z:βˆ‘(w:W)P(w))Q⁒(z) such that f⁒(c~′⁒(a,x))≑c⁒(a,x).

Proof.

Suppose given w:W and x:P⁒(w); we must produce an element f⁒(w,x):Q⁒(w,x). By inductionMathworldPlanetmath on w, it suffices to consider two cases. When w≑𝖼⁒(a), then we have x:C⁒(a), and so c⁒(a,x):Q⁒(𝖼⁒(a),x) as desired. (This part of the definition also ensures that the stated computational rule holds.)

Now we must show that this definition is preserved by transporting along 𝗉⁒(b) for any b:B. Since what we are defining, for all w:W, is a function of type ∏(x:P(w))Q⁒(w,x), by Lemma 2.9.7 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem2) it suffices to show that for any y:C⁒(f⁒(b)), we have

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—Q(𝗉𝖺𝗂𝗋=(𝗉(b),𝗋𝖾𝖿𝗅𝗉(b)*(y)),c(f(b),y))=c(g(b),𝗉(b)*(y)).

Let q:𝗉(b)*(y)=D(b)(y) be the path obtained from Lemma 6.12.1 (http://planetmath.org/612theflatteninglemma#Thmprelem1). Then we have

c(g(b),𝗉(b)*(y)) =π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦Q⁒(c⁒(g⁒(b),x))⁒(q-1,c⁒(g⁒(b),D⁒(b)⁒(y))) (by $\mathsf{apd}_{x\mapstoc(g(b),x)}(\mathord{{q}^{-1}})$)
=π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—Q⁒(𝖺𝗉x↦c⁒(g⁒(b),x)⁒(q-1),c⁒(g⁒(b),D⁒(b)⁒(y))). (by Lemma 2.3.10 (http://planetmath.org/23typefamiliesarefibrationshmprelem7))

Thus, it suffices to show

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—Q⁒(𝗉𝖺𝗂𝗋=⁒(𝗉⁒(b),𝗋𝖾𝖿𝗅𝗉(b)*(y)),c⁒(f⁒(b),y))=π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—Q⁒(𝖺𝗉x↦c⁒(g⁒(b),x)⁒(q-1),c⁒(g⁒(b),D⁒(b)⁒(y))).

Moving the right-hand transport to the other side, and combining two transports, this is equivalent to

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—Q⁒(𝖺𝗉x↦c⁒(g⁒(b),x)⁒(q)⁒\centerdot⁒𝗉𝖺𝗂𝗋=⁒(𝗉⁒(b),𝗋𝖾𝖿𝗅𝗉(b)*(y)),c⁒(f⁒(b),y))=c⁒(g⁒(b),D⁒(b)⁒(y)).

However, we have

𝖺𝗉x↦c⁒(g⁒(b),x)⁒(q)⁒\centerdot⁒𝗉𝖺𝗂𝗋=⁒(𝗉⁒(b),𝗋𝖾𝖿𝗅𝗉(b)*(y))=𝗉𝖺𝗂𝗋=⁒(𝗋𝖾𝖿𝗅g⁒(b),q)⁒\centerdot⁒𝗉𝖺𝗂𝗋=⁒(𝗉⁒(b),𝗋𝖾𝖿𝗅𝗉(b)*(y))=𝗉𝖺𝗂𝗋=⁒(𝗉⁒(b),q)=𝗉~′⁒(b,y)

so the construction is completed by the assumptionPlanetmathPlanetmath p⁒(b,y) of type

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—Q⁒(𝗉~′⁒(b,y),c⁒(f⁒(b),y))=c⁒(g⁒(b),D⁒(b)⁒(y)).∎

Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4) almost gives βˆ‘(w:W)P⁒(w) the same induction principle as W~. The missing bit is the equality 𝖺𝗉𝖽f⁒(𝗉~′⁒(b,y))=p⁒(b,y). In order to prove this, we would need to analyze the proof of Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4), which of course is the definition of f.

It should be possible to do this, but it turns out that we only need the computation rule for the non-dependent recursion principle. Thus, we now give a somewhat simpler direct construction of the recursor, and a proof of its computation rule.

Lemma 6.12.5.

Suppose Q is a type and that we have

  • β€’

    c:∏(a:A)C⁒(a)β†’Q and

  • β€’

    p:∏(b:B)∏(y:C(f(b)))(c(f(b),y)=Qc(g(b),D(b)(y))).

Then there exists f:(βˆ‘(w:W)P⁒(w))β†’Q such that f⁒(c~′⁒(a,x))≑c⁒(a,x).

Proof.

As in Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4), we define f⁒(w,x) by induction on w:W. When w≑𝖼⁒(a), we define f(𝖼(a),x):≑c(a,x). Now by Lemma 2.9.6 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem1), it suffices to consider, for b:B and y:C⁒(f⁒(b)), the composite path

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦Q⁒(𝗉⁒(b),c⁒(f⁒(b),y))=c⁒(g⁒(b),π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—P⁒(𝗉⁒(b),y)) (6.12.6)

defined as the compositionMathworldPlanetmath

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦Q⁒(𝗉⁒(b),c⁒(f⁒(b),y)) =c⁒(f⁒(b),y) (by Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrationshmprelem4))
=c⁒(g⁒(b),D⁒(b)⁒(y)) (by $p(b,y)$)
=c⁒(g⁒(b),π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—P⁒(𝗉⁒(b),y)). (by Lemma 6.12.1 (http://planetmath.org/612theflatteninglemmahmprelem1))

The computation rule f⁒(𝖼~′⁒(a,x))≑c⁒(a,x) follows by definition, as before. ∎

For the second computation rule, we need the following lemma.

Lemma 6.12.7.

Let Y:Xβ†’U be a type family and let f:(βˆ‘(x:X)Y⁒(x))β†’Z be defined componentwise by f(x,y):≑d(x)(y) for a curried function d:∏(x:X)Y⁒(x)β†’Z. Then for any s:x1=Xx2 and any y1:P⁒(x1) and y2:P⁒(x2) with a path r:s*(y1)=y2, the path

𝖺𝗉f⁒(𝗉𝖺𝗂𝗋=⁒(s,r)):f⁒(x1,y1)=f⁒(x2,y2)

is equal to the composite

f⁒(x1,y1) ≑d⁒(x1)⁒(y1)
=π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦Q⁒(s,d⁒(x1)⁒(y1)) (by $\mathord{{\text{(Lemma 2.3.5 ({http://planetmath.org/23typefamiliesarefibrationshmprelem4}))}}^{-1}}$)
=π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦Q(s,d(x1)(s-1*(s*(y1))))
=(π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦(Y(x)β†’Z)(s,d(x1)))(s*(y1)) (byΒ (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom0.E3))
=d(x2)(s*(y1)) (by $\mathsf{happly}(\mathsf{apd}_{d}(s))({s}_{*}\mathopen{}\left({y_{1}}\right)\mathclose{}$)
=d⁒(x2)⁒(y2) (by $\mathsf{ap}_{d(x_{2})}(r)$)
≑f⁒(x2,y2).
Proof.

After path induction on s and r, both equalities reduce to reflexivitiesMathworldPlanetmath. ∎

At first it may seem surprising that Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6) has such a complicated statement, while it can be proven so simply. The reason for the complication is to ensure that the statement is well-typed: 𝖺𝗉f⁒(𝗉𝖺𝗂𝗋=⁒(s,r)) and the composite path it is claimed to be equal to must both have the same start and end points. Once we have managed this, the proof is easy by path induction.

Lemma 6.12.8.

In the situation of Lemma 6.12.5 (http://planetmath.org/612theflatteninglemma#Thmprelem5), we have apf⁒(p~′⁒(b,y))=p⁒(b,y).

Proof.

Recall that 𝗉~β€²(b,y):≑𝗉𝖺𝗂𝗋=(𝗉(b),q) where q:𝗉(b)*(y)=D(b)(y) comes from Lemma 6.12.1 (http://planetmath.org/612theflatteninglemma#Thmprelem1). Thus, since f is defined componentwise, we may compute 𝖺𝗉f⁒(𝗉~′⁒(b,y)) by Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6), with

x1 :≑𝖼(f(b)) y1 :≑y
x2 :≑𝖼(g(b)) y2 :≑D(b)(y)
s :≑𝗉(b) r :≑q.

The curried function d:∏(w:W)P⁒(w)β†’Q was defined by induction on w:W; to apply Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6) we need to understand 𝖺𝗉d⁒(x2)⁒(r) and 𝗁𝖺𝗉𝗉𝗅𝗒(𝖺𝗉𝖽d(s),s*(y1)).

For the first, since d⁒(𝖼⁒(a),x)≑c⁒(a,x), we have

𝖺𝗉d⁒(x2)⁒(r)≑𝖺𝗉c⁒(g⁒(b),-)⁒(q).

For the second, the computation rule for the induction principle of W tells us that 𝖺𝗉𝖽d⁒(𝗉⁒(b)) is equal to the compositeΒ (6.12.6), passed across the equivalence of Lemma 2.9.6 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem1). Thus, the computation rule given in Lemma 2.9.6 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem1) implies that 𝗁𝖺𝗉𝗉𝗅𝗒(𝖺𝗉𝖽d(𝗉(b)),𝗉(b)*(y)) is equal to the composite

(𝗉(b)*(c(f(b),-)))(𝗉(b)*(y)) =𝗉(b)*(c(f(b),𝗉⁒(b)-1*(𝗉(b)*(y)))) (byΒ (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom0.E3))
=𝗉(b)*(c(f(b),y))
=c⁒(f⁒(b),y) (by Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrationshmprelem4))
=c⁒(f⁒(b),D⁒(b)⁒(y)) (by $p(b,y)$)
=c(f(b),𝗉(b)*(y)). (by $\mathord{{\mathsf{ap}_{c(g(b),-)}(q)}^{-1}}$)

Finally, substituting these values of 𝖺𝗉d⁒(x2)⁒(r) and 𝗁𝖺𝗉𝗉𝗅𝗒(𝖺𝗉𝖽d(s),s*(y1)) into Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6), we see that all the paths cancel out in pairs, leaving only p⁒(b,y). ∎

Now we are finally ready to prove the flattening lemma.

Proof of Lemma 6.12.2 (http://planetmath.org/612theflatteninglemma#Thmprelem2).

We define h:W~β†’βˆ‘(w:W)P⁒(w) by using the recursion principle for W~, with 𝖼~β€² and 𝗉~β€² as input data. Similarly, we define k:(βˆ‘(w:W)P⁒(w))β†’W~ by using the recursion principle of Lemma 6.12.5 (http://planetmath.org/612theflatteninglemma#Thmprelem5), with 𝖼~ and 𝗉~ as input data.

On the one hand, we must show that for any z:W~, we have k⁒(h⁒(z))=z. By induction on z, it suffices to consider the two constructors of W~. But we have

k⁒(h⁒(𝖼~⁒(a,x)))≑k⁒(𝖼~′⁒(a,x))≑𝖼~⁒(a,x)

by definition, while similarly

k(h(𝗉~(b,y)))=k(𝗉~β€²(b,y))=𝗉~(b,y)

using the propositional computation rule for W~ and Lemma 6.12.8 (http://planetmath.org/612theflatteninglemma#Thmprelem7).

On the other hand, we must show that for any z:βˆ‘(w:W)P⁒(w), we have h⁒(k⁒(z))=z. But this is essentially identical, using Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4) for β€œinduction on βˆ‘(w:W)P⁒(w)” and the same computation rules. ∎

Title 6.12 The flattening lemma
\metatable