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 $\mathcal{U}$ is a type universe, then we can define a type family $P:W\to\mathcal{U}$ 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 $\mathcal{U}$ , 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:\mathbb{S}^{1}\to\mathcal{U}$ by using $\mathbb{S}^{1}$ -recursion:

P(\mathsf{base}):\!\!\equiv X\qquad\text{and}\qquad{P}\mathopen{}\left({% \mathsf{loop}}\right)\mathclose{}:=\mathsf{ua}(e).

The type $X$ thus appears as the fiber $P(\mathsf{base})$ 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 $\mathsf{loop}$ .

Lemma 6.12.1.

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

\displaystyle\mathsf{transport}^{B}(p,u)

\displaystyle=e(u).

Proof.

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

	$\displaystyle\mathsf{transport}^{B}(p,u)$	$\displaystyle=\mathsf{idtoeqv}({B}\mathopen{}\left({p}\right)\mathclose{})(u)$
		$\displaystyle=\mathsf{idtoeqv}(\mathsf{ua}(e))(u)$
		$\displaystyle=e(u).\qed$

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\mathcal{U}$ is defined recursively as above, then its total space $\mathchoice{\sum_{x:W}\,}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{(x:W)}}{% \sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{(x:W)% }}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{(x% :W)}}{\sum_{(x:W)}}{\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, $\mathchoice{\sum_{x:W}\,}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{(x:W)}}{% \sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{(x:W)% }}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{(x% :W)}}{\sum_{(x:W)}}{\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:\mathcal{U}$ and $f,g:B\to{}A$ , and that the higher inductive type $W$ is generated by

•

$\mathsf{c}:A\to{}W$ and
•

$\mathsf{p}:\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}(\mathsf{c}(f(b))% =_{W}\mathsf{c}(g(b)))$ .

Thus, $W$ is the (homotopy) coequalizer of $f$ and $g$ . Using binary sums (coproducts) and dependent sums ( $\Sigma$ -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 $\mathbb{S}^{1}$ can be represented by taking $A:\!\!\equiv\mathbf{1}$ and $B:\!\!\equiv\mathbf{1}$ , 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{\mathsf{inl}}\circ j$ and $g:\!\!\equiv{\mathsf{inr}}\circ k$ .

Now suppose in addition that

•

$C:A\to\mathcal{U}$ is a family of types over $A$ , and
•

$D:\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:% B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}C(f(b))\simeq C(g(b))$ is a family of equivalences over $B$ .

Define a type family $P:W\to\mathcal{U}$ inductively by

	$\displaystyle P(\mathsf{c}(a))$	$\displaystyle:\!\!\equiv C(a)$
	$\displaystyle{P}\mathopen{}\left({\mathsf{p}(b)}\right)\mathclose{}$	$\displaystyle:=\mathsf{ua}(D(b)).$

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

•

$\widetilde{\mathsf{c}}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod% _{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}C(a)\to\widetilde{W}$ and
•

$\widetilde{\mathsf{p}}:\mathchoice{\prod_{(b:B)}\,}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{% \textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{% \mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b% :B)}}}\mathchoice{\prod_{(y:C(f(b)))}\,}{\mathchoice{{\textstyle\prod_{(y:C(f(% b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}{% \mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(% f(b)))}}{\prod_{(y:C(f(b)))}}}{\mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{% \prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}(\widetilde{% \mathsf{c}}(f(b),y)=_{\widetilde{W}}\widetilde{\mathsf{c}}(g(b),D(b)(y)))$ .

The flattening lemma is:

Lemma 6.12.2 (Flattening lemma).

In the above situation, we have

\Bigl{(}\mathchoice{\sum_{x:W}\,}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_{% (x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}}}{% \sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}% }}{\sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}P(x)\Bigr{)}\;\simeq\;\widetilde{% W}.

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

Lemma 6.12.3.

There are functions

•

$\widetilde{\mathsf{c}}^{\prime}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}C(a)\to\mathchoice{\sum_{x:W}\,}{\mathchoice{{\textstyle\sum_{(% x:W)}}}{\sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum% _{(x:W)}}}{\sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle% \sum_{(x:W)}}}{\sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}P(x)$ and
•

$\widetilde{\mathsf{p}}^{\prime}:\mathchoice{\prod_{(b:B)}\,}{\mathchoice{{% \textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{% \mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b% :B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{% \prod_{(b:B)}}}\mathchoice{\prod_{(y:C(f(b)))}\,}{\mathchoice{{\textstyle\prod% _{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}% }}{\mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y% :C(f(b)))}}{\prod_{(y:C(f(b)))}}}{\mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}% {\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}\Big{(}% \widetilde{\mathsf{c}}^{\prime}(f(b),y)=_{\mathchoice{\sum_{w:W}\,}{% \mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}% }}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:% W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{% (w:W)}}}P(w)}\widetilde{\mathsf{c}}^{\prime}(g(b),D(b)(y))\Big{)}$ .

Proof.

The first is easy; define $\widetilde{\mathsf{c}}^{\prime}(a,x):\!\!\equiv(\mathsf{c}(a),x)$ and note that by definition $P(\mathsf{c}(a))\equiv C(a)$ . For the second, suppose given $b : B$ and $y:C(f(b))$ ; we must give an equality

(\mathsf{c}(f(b)),y)=(\mathsf{c}(g(b),D(b)(y))).

Since we have $\mathsf{p}(b):f(b)=g(b)$ , by equalities in $\Sigma$ -types it suffices to give an equality ${\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{}=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 $\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{% \sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)% }}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w% :W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w)$ , it suffices to give analogous data as in the case of $\widetilde{W}$ .

Lemma 6.12.4.

Suppose $Q:\big{(}\mathchoice{\sum_{x:W}\,}{\mathchoice{{\textstyle\sum_{(x:W)}}}{\sum_% {(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}}}{% \sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}{\mathchoice{{\textstyle\sum_{(x:W)}% }}{\sum_{(x:W)}}{\sum_{(x:W)}}{\sum_{(x:W)}}}P(x)\big{)}\to\mathcal{U}$ is a type family and that we have

•

$c:\mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(x:C(a)% )}\,}{\mathchoice{{\textstyle\prod_{(x:C(a))}}}{\prod_{(x:C(a))}}{\prod_{(x:C(% a))}}{\prod_{(x:C(a))}}}{\mathchoice{{\textstyle\prod_{(x:C(a))}}}{\prod_{(x:C% (a))}}{\prod_{(x:C(a))}}{\prod_{(x:C(a))}}}{\mathchoice{{\textstyle\prod_{(x:C% (a))}}}{\prod_{(x:C(a))}}{\prod_{(x:C(a))}}{\prod_{(x:C(a))}}}Q(\widetilde{% \mathsf{c}}^{\prime}(a,x))$ and
•

$p:\mathchoice{\prod_{(b:B)}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(% b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\mathchoice{\prod_{(y:C(f(% b)))}\,}{\mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{% \prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}{\mathchoice{{\textstyle\prod_{(y:C(% f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}{% \mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(% f(b)))}}{\prod_{(y:C(f(b)))}}}\Big{(}{\widetilde{\mathsf{p}}^{\prime}(b,y)}_{*% }\mathopen{}\left({c(f(b),y)}\right)\mathclose{}=c(g(b),D(b)(y))\Big{)}$ .

Then there exists $f:\mathchoice{\prod_{z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{% (w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle% \sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{% \textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w)}\,}{% \mathchoice{{\textstyle\prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{% \textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{% \mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}% }}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:% W)}}}P(w))}}}{\prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_% {(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle% \sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{% \textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))}}{% \prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum% _{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{% \sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}% }}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))}}{\prod_{(z:\mathchoice{% \sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}% }{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:% W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{% (w:W)}}{\sum_{(w:W)}}}P(w))}}}{\mathchoice{{\textstyle\prod_{(z:\mathchoice{% \sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}% }{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:% W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{% (w:W)}}{\sum_{(w:W)}}}P(w))}}}{\prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice% {{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{% \mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}% }}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:% W)}}}P(w))}}{\prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{% (w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle% \sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{% \textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))}}{% \prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum% _{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{% \sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}% }}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))}}}{\mathchoice{{\textstyle% \prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum% _{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{% \sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}% }}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))}}}{\prod_{(z:\mathchoice{% \sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}% }{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:% W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{% (w:W)}}{\sum_{(w:W)}}}P(w))}}{\prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{% {\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{% \mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}% }}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:% W)}}}P(w))}}{\prod_{(z:\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{% (w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle% \sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{% \textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))}}}Q(z)$ such that $f(\widetilde{\mathsf{c}}^{\prime}(a,x))\equiv c(a,x)$ .

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\mathsf{c}(a)$ , then we have $x:C(a)$ , and so $c(a,x):Q(\mathsf{c}(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 $\mathsf{p}(b)$ for any $b : B$ . Since what we are defining, for all $w : W$ , is a function of type $\mathchoice{\prod_{x:P(w)}\,}{\mathchoice{{\textstyle\prod_{(x:P(w))}}}{\prod_% {(x:P(w))}}{\prod_{(x:P(w))}}{\prod_{(x:P(w))}}}{\mathchoice{{\textstyle\prod_% {(x:P(w))}}}{\prod_{(x:P(w))}}{\prod_{(x:P(w))}}{\prod_{(x:P(w))}}}{% \mathchoice{{\textstyle\prod_{(x:P(w))}}}{\prod_{(x:P(w))}}{\prod_{(x:P(w))}}{% \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

\mathsf{transport}^{Q}(\mathsf{pair}^{\mathord{=}}(\mathsf{p}(b),\mathsf{refl}% _{{\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{}}),c(f(b),y))=c(g(% b),{\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{}).

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

	$\displaystyle c(g(b),{\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{})$	$\displaystyle=\mathsf{transport}^{x\mapsto Q(c(g(b),x))}(\mathord{{q}^{-1}},c(% g(b),D(b)(y))){}$		(by $\mathsf{apd}_{x\mapstoc(g(b),x)}(\mathord{{q}^{-1}})$)
		$\displaystyle=\mathsf{transport}^{Q}(\mathsf{ap}_{x\mapsto c(g(b),x)}(\mathord% {{q}^{-1}}),c(g(b),D(b)(y))){}.$		(by Lemma 2.3.10 (http://planetmath.org/23typefamiliesarefibrationshmprelem7))

Thus, it suffices to show

\displaystyle\mathsf{transport}^{Q}\Big{(}\mathsf{pair}^{\mathord{=}}(\mathsf{% p}(b),\mathsf{refl}_{{\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{% }}),\,c(f(b),y)\Big{)}=\\ \displaystyle\mathsf{transport}^{Q}\Big{(}\mathsf{ap}_{x\mapsto c(g(b),x)}(% \mathord{{q}^{-1}}),\,c(g(b),D(b)(y))\Big{)}.

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

\mathsf{transport}^{Q}\Big{(}\mathsf{ap}_{x\mapsto c(g(b),x)}(q)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{% pair}^{\mathord{=}}(\mathsf{p}(b),\mathsf{refl}_{{\mathsf{p}(b)}_{*}\mathopen{% }\left({y}\right)\mathclose{}}),\,c(f(b),y)\Big{)}=c(g(b),D(b)(y)).

However, we have

\displaystyle\mathsf{ap}_{x\mapsto c(g(b),x)}(q)\mathchoice{\mathbin{\raisebox% {2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}% }}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{pair}^{\mathord% {=}}(\mathsf{p}(b),\mathsf{refl}_{{\mathsf{p}(b)}_{*}\mathopen{}\left({y}% \right)\mathclose{}})=\\ \displaystyle\mathsf{pair}^{\mathord{=}}(\mathsf{refl}_{g(b)},q)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{% pair}^{\mathord{=}}(\mathsf{p}(b),\mathsf{refl}_{{\mathsf{p}(b)}_{*}\mathopen{% }\left({y}\right)\mathclose{}})=\mathsf{pair}^{\mathord{=}}(\mathsf{p}(b),q)=% \widetilde{\mathsf{p}}^{\prime}(b,y)

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

\mathsf{transport}^{Q}(\widetilde{\mathsf{p}}^{\prime}(b,y),c(f(b),y))=c(g(b),% D(b)(y)).\qed

Lemma 6.12.4 (http://planetmath.org/612theflatteninglemma#Thmprelem4) almost gives $\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)}}{% \sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)% }}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w% :W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w)$ the same induction principle as $\widetilde{W}$ . The missing bit is the equality $\mathsf{apd}_{f}(\widetilde{\mathsf{p}}^{\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:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}C(a)\to Q$ and
•

$p:\mathchoice{\prod_{(b:B)}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(% b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\mathchoice{\prod_{(y:C(f(% b)))}\,}{\mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{% \prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}{\mathchoice{{\textstyle\prod_{(y:C(% f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(f(b)))}}}{% \mathchoice{{\textstyle\prod_{(y:C(f(b)))}}}{\prod_{(y:C(f(b)))}}{\prod_{(y:C(% f(b)))}}{\prod_{(y:C(f(b)))}}}\Big{(}c(f(b),y)=_{Q}c(g(b),D(b)(y))\Big{)}$ .

Then there exists $f:\big{(}\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_% {(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{% \sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}% }}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w)\big{)}\to Q$ such that $f(\widetilde{\mathsf{c}}^{\prime}(a,x))\equiv 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\equiv\mathsf{c}(a)$ , we define $f(\mathsf{c}(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

\mathsf{transport}^{x\mapsto Q}(\mathsf{p}(b),c(f(b),y))=c(g(b),\mathsf{% transport}^{P}(\mathsf{p}(b),y))

(6.12.6)

defined as the composition

$\displaystyle\mathsf{transport}^{x\mapsto Q}(\mathsf{p}(b),c(f(b),y))$	$\displaystyle=c(f(b),y){}$	(by Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrationshmprelem4))
	$\displaystyle=c(g(b),D(b)(y)){}$	(by $p(b,y)$)
	$\displaystyle=c(g(b),\mathsf{transport}^{P}(\mathsf{p}(b),y)).{}$	(by Lemma 6.12.1 (http://planetmath.org/612theflatteninglemmahmprelem1))

The computation rule $f(\widetilde{\mathsf{c}}^{\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:X\to\mathcal{U}$ be a type family and let $f:(\mathchoice{\sum_{x:X}\,}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)% }}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x% :X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_% {(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}Y(x))\to Z$ be defined componentwise by $f(x,y):\!\!\equiv d(x)(y)$ for a curried function $d:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}Y(x)\to Z$ . Then for any $s:x_{1}=_{X}x_{2}$ and any $y_{1}:P(x_{1})$ and $y_{2}:P(x_{2})$ with a path $r:{s}_{*}\mathopen{}\left({y_{1}}\right)\mathclose{}=y_{2}$ , the path

\mathsf{ap}_{f}(\mathsf{pair}^{\mathord{=}}(s,r)):f(x_{1},y_{1})=f(x_{2},y_{2})

is equal to the composite

$\displaystyle f(x_{1},y_{1})$	$\displaystyle\equiv d(x_{1})(y_{1})$
	$\displaystyle=\mathsf{transport}^{x\mapsto Q}(s,d(x_{1})(y_{1})){}$	(by $\mathord{{\text{(Lemma 2.3.5 ({http://planetmath.org/23typefamiliesarefibrationshmprelem4}))}}^{-1}}$)
	$\displaystyle=\mathsf{transport}^{x\mapsto Q}(s,d(x_{1})({\mathord{{s}^{-1}}}_% {}\mathopen{}\left({{s}_{}\mathopen{}\left({y_{1}}\right)\mathclose{}}\right% )\mathclose{}))$
	$\displaystyle=\big{(}\mathsf{transport}^{x\mapsto(Y(x)\to Z)}(s,d(x_{1}))\big{% )}({s}_{*}\mathopen{}\left({y_{1}}\right)\mathclose{}){}$	(by (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom0.E3))
	$\displaystyle=d(x_{2})({s}_{*}\mathopen{}\left({y_{1}}\right)\mathclose{}){}$	(by $\mathsf{happly}(\mathsf{apd}_{d}(s))({s}_{*}\mathopen{}\left({y_{1}}\right)\mathclose{}$)
	$\displaystyle=d(x_{2})(y_{2}){}$	(by $\mathsf{ap}_{d(x_{2})}(r)$)
	$\displaystyle\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: $\mathsf{ap}_{f}(\mathsf{pair}^{\mathord{=}}(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 $\mathsf{ap}_{f}(\widetilde{\mathsf{p}}^{\prime}(b,y))=p(b,y)$ .

Proof.

Recall that $\widetilde{\mathsf{p}}^{\prime}(b,y):\!\!\equiv\mathsf{pair}^{\mathord{=}}(% \mathsf{p}(b),q)$ where $q:{\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{}=D(b)(y)$ comes from Lemma 6.12.1 (http://planetmath.org/612theflatteninglemma#Thmprelem1). Thus, since $f$ is defined componentwise, we may compute $\mathsf{ap}_{f}(\widetilde{\mathsf{p}}^{\prime}(b,y))$ by Lemma 6.12.7 (http://planetmath.org/612theflatteninglemma#Thmprelem6), with

$\displaystyle x_{1}$	$\displaystyle:\!\!\equiv\mathsf{c}(f(b))$	$\displaystyle y_{1}$	$\displaystyle:\!\!\equiv y$
$\displaystyle x_{2}$	$\displaystyle:\!\!\equiv\mathsf{c}(g(b))$	$\displaystyle y_{2}$	$\displaystyle:\!\!\equiv D(b)(y)$
$\displaystyle s$	$\displaystyle:\!\!\equiv\mathsf{p}(b)$	$\displaystyle r$	$\displaystyle:\!\!\equiv q.$

The curried function $d:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:% W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{% \prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w% :W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\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 $\mathsf{ap}_{d(x_{2})}(r)$ and $\mathsf{happly}(\mathsf{apd}_{d}(s),{s}_{*}\mathopen{}\left({y_{1}}\right)% \mathclose{})$ .

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

\mathsf{ap}_{d(x_{2})}(r)\equiv\mathsf{ap}_{c(g(b),-)}(q).

For the second, the computation rule for the induction principle of $W$ tells us that $\mathsf{apd}_{d}(\mathsf{p}(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 $\mathsf{happly}(\mathsf{apd}_{d}(\mathsf{p}(b)),{\mathsf{p}(b)}_{*}\mathopen{}% \left({y}\right)\mathclose{})$ is equal to the composite

$\displaystyle\big{(}{\mathsf{p}(b)}_{}\mathopen{}\left({c(f(b),-)}\right)% \mathclose{}\big{)}({\mathsf{p}(b)}_{}\mathopen{}\left({y}\right)\mathclose{})$	$\displaystyle={\mathsf{p}(b)}_{}\mathopen{}\left({c(f(b),{\mathord{{\mathsf{p% }(b)}^{-1}}}_{}\mathopen{}\left({{\mathsf{p}(b)}_{*}\mathopen{}\left({y}% \right)\mathclose{}}\right)\mathclose{})}\right)\mathclose{}{}$	(by (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom0.E3))
	$\displaystyle={\mathsf{p}(b)}_{*}\mathopen{}\left({c(f(b),y)}\right)\mathclose{}$
	$\displaystyle=c(f(b),y){}$	(by Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrationshmprelem4))
	$\displaystyle=c(f(b),D(b)(y)){}$	(by $p(b,y)$)
	$\displaystyle=c(f(b),{\mathsf{p}(b)}_{*}\mathopen{}\left({y}\right)\mathclose{% }).{}$	(by $\mathord{{\mathsf{ap}_{c(g(b),-)}(q)}^{-1}}$)

Finally, substituting these values of $\mathsf{ap}_{d(x_{2})}(r)$ and $\mathsf{happly}(\mathsf{apd}_{d}(s),{s}_{*}\mathopen{}\left({y_{1}}\right)% \mathclose{})$ 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:\widetilde{W}\to\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)% }}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w% :W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_% {(w:W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w)$ by using the recursion principle for $\widetilde{W}$ , with $\widetilde{\mathsf{c}}^{\prime}$ and $\widetilde{\mathsf{p}}^{\prime}$ as input data. Similarly, we define $k:(\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w:W)% }}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_{(w% :W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}}}{\sum_% {(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}P(w))\to\widetilde{W}$ by using the recursion principle of Lemma 6.12.5 (http://planetmath.org/612theflatteninglemma#Thmprelem5), with $\widetilde{\mathsf{c}}$ and $\widetilde{\mathsf{p}}$ as input data.

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

k(h(\widetilde{\mathsf{c}}(a,x)))\equiv k(\widetilde{\mathsf{c}}^{\prime}(a,x)% )\equiv\widetilde{\mathsf{c}}(a,x)

by definition, while similarly

{k}\mathopen{}\left({{h}\mathopen{}\left({\widetilde{\mathsf{p}}(b,y)}\right)% \mathclose{}}\right)\mathclose{}={k}\mathopen{}\left({\widetilde{\mathsf{p}}^{% \prime}(b,y)}\right)\mathclose{}=\widetilde{\mathsf{p}}(b,y)

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

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

Title	6.12 The flattening lemma
\metatable