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 universe, then we can define a type family $P:W\to 𝒰$ 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\simeq X$.Then we can define a type family $P:{𝕊}^1\to 𝒰$ by using ${𝕊}^1$-recursion:

$$P(\mathrm{𝖻𝖺𝗌𝖾}):\equiv X\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}P\left(\mathrm{𝗅𝗈𝗈𝗉}\right):=\mathrm{𝗎𝖺}(e).$$

The type $X$ thus appears as the fiber $P(\mathrm{𝖻𝖺𝗌𝖾})$ 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 $\mathrm{𝗅𝗈𝗈𝗉}$.

Lemma 6.12.1.

Given $B\mathrm{:}A\mathrm{\to }\mathrm{U}$ and $x\mathrm{,}y\mathrm{:}A$, with a path $p\mathrm{:}x\mathrm{=}y$ and an equivalence $e\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\simeq }P\mathit{}\mathrm{(}y\mathrm{)}$ such that $B\mathrm{\left(}p\mathrm{\right)}\mathrm{=}\mathrm{ua}\mathrm{(}e\mathrm{)}$, then for any $u\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}$ we have

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,u)$$=e(u).$

Proof.

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

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,u)$$=\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(B\left(p\right))(u)$

$=\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(\mathrm{𝗎𝖺}(e))(u)$

$=e(u).\mathit{∎}$

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 section, 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\to 𝒰$ is defined recursively as above, then its total space ${\sum }_{(x:W)}P(x)$ is equivalent 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, ${\sum }_{(x:W)}P(x)$ is the “Grothendieck construction” of $P$, and this expresses its universal property as a “lax colimit”.

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\to A$, and that the higher inductive type $W$ is generated by

• $𝖼:A\to W$ and

• $𝗉:{\prod }_{(b:B)}(𝖼(f(b)){=}_W𝖼(g(b)))$.

Thus, $W$ is the (homotopy) coequalizerof $f$ and $g$.Using binary sums (coproducts) and dependent sums ($\mathrm{\Sigma }$-types), a lot of interesting nonrecursive higherinductive types can be represented in this form. All point constructors have tobe bundled in the type $A$ and all path constructors in the type $B$.For instance:

• The circle ${𝕊}^1$ can be represented by taking $A:\equiv \mathrm{𝟏}$ and $B:\equiv \mathrm{𝟏}$, with $f$ and $g$ the identity.

• The pushout of $j:X\to Y$ and $k:X\to Z$ can be represented by taking $A:\equiv Y+Z$ and $B:\equiv X$, with $f:\equiv \mathrm{𝗂𝗇𝗅}\circ j$ and $g:\equiv \mathrm{𝗂𝗇𝗋}\circ k$.

Now suppose in addition that

• $C:A\to 𝒰$ is a family of types over $A$, and

• $D:{\prod }_{(b:B)}C(f(b))\simeq C(g(b))$ is a family of equivalences over $B$.

Define a type family $P:W\to 𝒰$ inductively by

$P(𝖼(a))$$:\equiv C(a)$

$P\left(𝗉(b)\right)$$:=\mathrm{𝗎𝖺}(D(b)).$

Let $\tilde{W}$ be the higher inductive type generated by

• $\widetilde{𝖼}:{\prod }_{(a:A)}C(a)\to \tilde{W}$ and

• $\widetilde{𝗉}:{\prod }_{(b:B)}{\prod }_{(y:C(f(b)))}(\widetilde{𝖼}(f(b),y){=}_{\tilde{W}}\widetilde{𝖼}(g(b),D(b)(y)))$.

The flattening lemma is:

Lemma 6.12.2 (Flattening lemma).

In the above situation, we have

$$\left(\sum _{x:W}P(x)\right)\simeq \tilde{W}.$$

As remarked above, this equivalence can be seen as expressing the universal property of ${\sum }_{(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 ${\sum }_{(x:W)}P(x)$ has the same universal property as $\tilde{W}$.We begin by showing that it comes with analogues of the constructors $\widetilde{𝖼}$ and $\widetilde{𝗉}$.

Lemma 6.12.3.

There are functions

• ${\widetilde{𝖼}}^{\prime }:{\prod }_{(a:A)}C(a)\to {\sum }_{(x:W)}P(x)$ and

• ${\widetilde{𝗉}}^{\prime }:{\prod }_{(b:B)}{\prod }_{(y:C(f(b)))}\left({\widetilde{𝖼}}^{\prime }(f(b),y){=}_{{\sum }_{(w:W)}P(w)}{\widetilde{𝖼}}^{\prime }(g(b),D(b)(y))\right)$.

Proof.

The first is easy; define ${\widetilde{𝖼}}^{\prime }(a,x):\equiv (𝖼(a),x)$ and note that by definition $P(𝖼(a))\equiv 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 $\mathrm{\Sigma }$-types it suffices to give an equality $𝗉{(b)}_{*}\left(y\right)=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 ${\sum }_{(w:W)}P(w)$, it suffices to give analogous data as in the case of $\tilde{W}$.

Lemma 6.12.4.

Suppose $Q\mathrm{:}\mathrm{\left(}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}W\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\right)}\mathrm{\to }\mathrm{U}$ is a type family and that we have

• $c:{\prod }_{(a:A)}{\prod }_{(x:C(a))}Q({\widetilde{𝖼}}^{\prime }(a,x))$ and

• $p:{\prod }_{(b:B)}{\prod }_{(y:C(f(b)))}({\widetilde{𝗉}}^{\prime }{(b,y)}_{*}\left(c(f(b),y)\right)=c(g(b),D(b)(y)))$.

Then there exists $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}z\mathrm{:}{\mathrm{\sum }}_{\mathrm{(}w\mathrm{:}W\mathrm{)}}P\mathrm{(}w\mathrm{)}\mathrm{)}}Q\mathit{}\mathrm{(}z\mathrm{)}$ such that $f\mathit{}\mathrm{(}{\stackrel{\mathrm{~}}{\mathrm{c}}}^{\mathrm{\prime }}\mathit{}\mathrm{(}a\mathrm{,}x\mathrm{)}\mathrm{)}\mathrm{\equiv }c\mathit{}\mathrm{(}a\mathrm{,}x\mathrm{)}$.

Proof.

Suppose given $w:W$ and $x:P(w)$; we must produce an element $f(w,x):Q(w,x)$.By induction on $w$, it suffices to consider two cases.When $w\equiv 𝖼(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 ${\prod }_{(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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),{\mathrm{𝗋𝖾𝖿𝗅}}_{𝗉{(b)}_{*}\left(y\right)}),c(f(b),y))=c(g(b),𝗉{(b)}_{*}\left(y\right)).$$

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

$c(g(b),𝗉{(b)}_{*}\left(y\right))$$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto Q(c(g(b),x))}(q^{-1},c(g(b),D(b)(y)))$(by $\\mathsf{apd}_{x\\mapstoc(g(b),x)}(\\mathord{{q}^{-1}})$)

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q({\mathrm{𝖺𝗉}}_{x\mapsto 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

$$\begin{array}{c}{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),{\mathrm{𝗋𝖾𝖿𝗅}}_{𝗉{(b)}_{*}\left(y\right)}),c(f(b),y))=\hfill \\ \hfill {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q({\mathrm{𝖺𝗉}}_{x\mapsto c(g(b),x)}(q^{-1}),c(g(b),D(b)(y))).\end{array}$$

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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q({\mathrm{𝖺𝗉}}_{x\mapsto c(g(b),x)}(q){\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),{\mathrm{𝗋𝖾𝖿𝗅}}_{𝗉{(b)}_{*}\left(y\right)}),c(f(b),y))=c(g(b),D(b)(y)).$$

However, we have

$$\begin{array}{c}{\mathrm{𝖺𝗉}}_{x\mapsto c(g(b),x)}(q){\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),{\mathrm{𝗋𝖾𝖿𝗅}}_{𝗉{(b)}_{*}\left(y\right)})=\hfill \\ \hfill {\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}({\mathrm{𝗋𝖾𝖿𝗅}}_{g(b)},q){\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),{\mathrm{𝗋𝖾𝖿𝗅}}_{𝗉{(b)}_{*}\left(y\right)})={\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),q)={\widetilde{𝗉}}^{\prime }(b,y)\end{array}$$

so the construction is completed by the assumption $p(b,y)$ of type

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q({\widetilde{𝗉}}^{\prime }(b,y),c(f(b),y))=c(g(b),D(b)(y)).\mathit{∎}$$

Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4) almost gives ${\sum }_{(w:W)}P(w)$ the same induction principle as $\tilde{W}$.The missing bit is the equality ${\mathrm{𝖺𝗉𝖽}}_f({\widetilde{𝗉}}^{\prime }(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:{\prod }_{(a:A)}C(a)\to Q$ and

• $p:{\prod }_{(b:B)}{\prod }_{(y:C(f(b)))}\left(c(f(b),y){=}_{Q}c(g(b),D(b)(y))\right)$.

Then there exists $f\mathrm{:}\mathrm{\left(}{\mathrm{\sum }}_{\mathrm{(}w\mathrm{:}W\mathrm{)}}P\mathit{}\mathrm{(}w\mathrm{)}\mathrm{\right)}\mathrm{\to }Q$ such that $f\mathit{}\mathrm{(}{\stackrel{\mathrm{~}}{\mathrm{c}}}^{\mathrm{\prime }}\mathit{}\mathrm{(}a\mathrm{,}x\mathrm{)}\mathrm{)}\mathrm{\equiv }c\mathit{}\mathrm{(}a\mathrm{,}x\mathrm{)}$.

Proof.

As in Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4), we define $f(w,x)$ by induction on $w:W$.When $w\equiv 𝖼(a)$, we define $f(𝖼(a),x):\equiv 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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto Q}(𝗉(b),c(f(b),y))=c(g(b),{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(𝗉(b),y))$$(6.12.6)

defined as the composition

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto 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),{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(𝗉(b),y)).$(by Lemma 6.12.1 (http://planetmath.org/612theflatteninglemmahmprelem1))

The computation rule $f({\widetilde{𝖼}}^{\prime }(a,x))\equiv c(a,x)$ follows by definition, as before.∎

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

Lemma 6.12.7.

Let $Y\mathrm{:}X\mathrm{\to }\mathrm{U}$ be a type family and let $f\mathrm{:}\mathrm{(}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}X\mathrm{)}}Y\mathit{}\mathrm{(}x\mathrm{)}\mathrm{)}\mathrm{\to }Z$ be defined componentwise by $f\mathrm{(}x\mathrm{,}y\mathrm{)}\mathrm{:}\mathrm{\equiv }d\mathrm{(}x\mathrm{)}\mathrm{(}y\mathrm{)}$ for a curried function $d\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}X\mathrm{)}}Y\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\to }Z$.Then for any $s\mathrm{:}{x}_{\mathrm{1}}{\mathrm{=}}_X{x}_{\mathrm{2}}$ and any $y_{\mathrm{1}}\mathrm{:}P\mathit{}\mathrm{(}{x}_{\mathrm{1}}\mathrm{)}$ and $y_{\mathrm{2}}\mathrm{:}P\mathit{}\mathrm{(}{x}_{\mathrm{2}}\mathrm{)}$ with a path $r\mathrm{:}{s}_{\mathrm{*}}\mathrm{\left(}{y}_{\mathrm{1}}\mathrm{\right)}\mathrm{=}{y}_{\mathrm{2}}$, the path

$${\mathrm{𝖺𝗉}}_f({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(s,r)):f(x_1,y_1)=f(x_2,y_2)$$

is equal to the composite

$f(x_1,y_1)$$\equiv d(x_1)(y_1)$

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto Q}(s,d(x_1)(y_1))$(by $\\mathord{{\\text{(Lemma 2.3.5 ({http://planetmath.org/23typefamiliesarefibrationshmprelem4}))}}^{-1}}$)

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto Q}(s,d(x_1)(s^{-1}{}_{*}\left(s_{*}\left(y_1\right)\right)))$

$=\left({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto (Y(x)\to Z)}(s,d(x_1))\right)(s_{*}\left(y_1\right))$(by (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom0.E3))

$=d(x_2)(s_{*}\left(y_1\right))$(by $\\mathsf{happly}(\\mathsf{apd}_{d}(s))({s}_{*}\\mathopen{}\\left({y_{1}}\\right)\\mathclose{}$)

$=d(x_2)(y_2)$(by $\\mathsf{ap}_{d(x_{2})}(r)$)

$\equiv f(x_2,y_2).$

Proof.

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

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: ${\mathrm{𝖺𝗉}}_f({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(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 ${\mathrm{ap}}_f\mathit{}\mathrm{(}{\stackrel{\mathrm{~}}{\mathrm{p}}}^{\mathrm{\prime }}\mathit{}\mathrm{(}b\mathrm{,}y\mathrm{)}\mathrm{)}\mathrm{=}p\mathit{}\mathrm{(}b\mathrm{,}y\mathrm{)}$.

Proof.

Recall that ${\widetilde{𝗉}}^{\prime }(b,y):\equiv {\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(𝗉(b),q)$ where $q:𝗉{(b)}_{*}\left(y\right)=D(b)(y)$ comes from Lemma 6.12.1 (http://planetmath.org/612theflatteninglemma#Thmprelem1).Thus, since $f$ is defined componentwise, we may compute ${\mathrm{𝖺𝗉}}_f({\widetilde{𝗉}}^{\prime }(b,y))$ by Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6), with

$x_1$$:\equiv 𝖼(f(b))$$y_1$$:\equiv y$

$x_2$$:\equiv 𝖼(g(b))$$y_2$$:\equiv D(b)(y)$

$s$$:\equiv 𝗉(b)$$r$$:\equiv q.$

The curried function $d:{\prod }_{(w:W)}P(w)\to Q$ was defined by induction on $w:W$;to apply Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6) we need to understand ${\mathrm{𝖺𝗉}}_{d(x_2)}(r)$ and $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}({\mathrm{𝖺𝗉𝖽}}_d(s),s_{*}\left(y_1\right))$.

For the first, since $d(𝖼(a),x)\equiv c(a,x)$, we have

$${\mathrm{𝖺𝗉}}_{d(x_2)}(r)\equiv {\mathrm{𝖺𝗉}}_{c(g(b),-)}(q).$$

For the second, the computation rule for the induction principle of $W$ tells us that ${\mathrm{𝖺𝗉𝖽}}_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 $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}({\mathrm{𝖺𝗉𝖽}}_d(𝗉(b)),𝗉{(b)}_{*}\left(y\right))$ is equal to the composite

$\left(𝗉{(b)}_{*}\left(c(f(b),-)\right)\right)(𝗉{(b)}_{*}\left(y\right))$$=𝗉{(b)}_{*}\left(c(f(b),{𝗉{(b)}^{-1}}_{*}\left(𝗉{(b)}_{*}\left(y\right)\right))\right)$(by (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom0.E3))

$=𝗉{(b)}_{*}\left(c(f(b),y)\right)$

$=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)}_{*}\left(y\right)).$(by $\\mathord{{\\mathsf{ap}_{c(g(b),-)}(q)}^{-1}}$)

Finally, substituting these values of ${\mathrm{𝖺𝗉}}_{d(x_2)}(r)$ and $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}({\mathrm{𝖺𝗉𝖽}}_d(s),s_{*}\left(y_1\right))$ 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:\tilde{W}\to {\sum }_{(w:W)}P(w)$ by using the recursion principle for $\tilde{W}$, with ${\widetilde{𝖼}}^{\prime }$ and ${\widetilde{𝗉}}^{\prime }$ as input data.Similarly, we define $k:({\sum }_{(w:W)}P(w))\to \tilde{W}$ by using the recursion principle of Lemma 6.12.5 (http://planetmath.org/612theflatteninglemma#Thmprelem5), with $\widetilde{𝖼}$ and $\widetilde{𝗉}$ as input data.

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

$$k(h(\widetilde{𝖼}(a,x)))\equiv k({\widetilde{𝖼}}^{\prime }(a,x))\equiv \widetilde{𝖼}(a,x)$$

by definition, while similarly

$$k\left(h\left(\widetilde{𝗉}(b,y)\right)\right)=k\left({\widetilde{𝗉}}^{\prime }(b,y)\right)=\widetilde{𝗉}(b,y)$$

using the propositional computation rule for $\tilde{W}$ and Lemma 6.12.8 (http://planetmath.org/612theflatteninglemma#Thmprelem7).

On the other hand, we must show that for any $z:{\sum }_{(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 ${\sum }_{(w:W)}P(w)$” and the same computation rules.∎