8.5.1 Fibrations over pushouts

We first start with a lemma explaining how to construct fibrations over pushouts.

Lemma 8.5.1.

Let $\mathscr{D}=(Y\xleftarrow{j}X\xrightarrow{k}Z)$ be a span and assume that we have

•

Two fibrations $E_{Y}:Y\to\mathcal{U}$ and $E_{Z}:Z\to\mathcal{U}$ .
•

An equivalence $e_{X}$ between $E_{Y}\circ j:X\to\mathcal{U}$ and $E_{Z}\circ k:X\to\mathcal{U}$ , i.e.

$e_{X}:\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)}}}E_{Y}(j(x))\simeq E_{Z}(k% (x)).$

Then we can construct a fibration $E:Y\sqcup^{X}Z\to\mathcal{U}$ such that

•

For all $y : Y$ , $E({\mathsf{inl}}(y))\equiv E_{Y}(y)$ .
•

For all $z : Z$ , $E({\mathsf{inr}}(z))\equiv E_{Z}(z)$ .
•

For all $x : X$ , ${E}\mathopen{}\left({\mathsf{glue}(x)}\right)\mathclose{}=\mathsf{ua}(e_{X}(x))$ (note that both sides of the equation are paths in $\mathcal{U}$ from $E_{Y}(j(x))$ to $E_{Z}(k(x))$ ).

Moreover, the total space of this fibration fits in the following pushout square:

\xymatrix{\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)}}}E_{Y}(j(x))\ar[r]_{\sim}^{\mathsf% {id}\times e_{X}}\ar[d]_{j\times\mathsf{id}}&\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)}}}E_{Z}(k(x))\ar[r]^{-}{k\times\mathsf{id}}&\mathchoice{\sum_{z:Z}\,}{% \mathchoice{{\textstyle\sum_{(z:Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:Z)}% }}{\mathchoice{{\textstyle\sum_{(z:Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:% Z)}}}{\mathchoice{{\textstyle\sum_{(z:Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{% (z:Z)}}}E_{Z}(z)\ar[d]^{\mathsf{inr}}\\ \mathchoice{\sum_{y:Y}\,}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)}}{% \sum_{(y:Y)}}{\sum_{(y:Y)}}}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)% }}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y% :Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}E_{Y}(y)\ar[rr]_{\mathsf{inl}}&&\mathchoice{% \sum_{t:Y\sqcup^{X}Z}\,}{\mathchoice{{\textstyle\sum_{(t:Y\sqcup^{X}Z)}}}{\sum% _{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}}{% \mathchoice{{\textstyle\sum_{(t:Y\sqcup^{X}Z)}}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum% _{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}}{\mathchoice{{\textstyle\sum_{(t% :Y\sqcup^{X}Z)}}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y% \sqcup^{X}Z)}}}E(t)}

Proof.

We define $E$ by the recursion principle of the pushout $Y\sqcup^{X}Z$ . For that, we need to specify the value of $E$ on elements of the form ${\mathsf{inl}}(y)$ , ${\mathsf{inr}}(z)$ and the action of $E$ on paths $\mathsf{glue}(x)$ , so we can just choose the following values:

	$\displaystyle E({\mathsf{inl}}(y))$	$\displaystyle:\!\!\equiv E_{Y}(y),$
	$\displaystyle E({\mathsf{inr}}(z))$	$\displaystyle:\!\!\equiv E_{Z}(z),$
	$\displaystyle{E}\mathopen{}\left({\mathsf{glue}(x)}\right)\mathclose{}$	$\displaystyle\coloneqq\mathsf{ua}(e_{X}(x)).$

To see that the total space of this fibration is a pushout, we apply the flattening lemma (\autorefthm:flattening) with the following values:

•

$A:\!\!\equiv Y+Z$ , $B:\!\!\equiv X$ and $f,g:B\to A$ are defined by $f(x):\!\!\equiv{\mathsf{inl}}(j(x))$ , $g(x):\!\!\equiv{\mathsf{inr}}(k(x))$ ,
•

the type family $C:A\to\mathcal{U}$ is defined by

$C({\mathsf{inl}}(y)):\!\!\equiv E_{Y}(y)\qquad\text{and}\qquad C({\mathsf{inr}% }(z)):\!\!\equiv E_{Z}(z),$
•

the family of equivalences $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 defined to be $e_{X}$ .

The base higher inductive type $W$ in the flattening lemma is equivalent to the pushout $Y\sqcup^{X}Z$ and the type family $P:Y\sqcup^{X}Z\to\mathcal{U}$ is equivalent to the $E$ defined above.

Thus the flattening lemma tells us that $\mathchoice{\sum_{t:Y\sqcup^{X}Z}\,}{\mathchoice{{\textstyle\sum_{(t:Y\sqcup^{% X}Z)}}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}% Z)}}}{\mathchoice{{\textstyle\sum_{(t:Y\sqcup^{X}Z)}}}{\sum_{(t:Y\sqcup^{X}Z)}% }{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}}{\mathchoice{{\textstyle% \sum_{(t:Y\sqcup^{X}Z)}}}{\sum_{(t:Y\sqcup^{X}Z)}}{\sum_{(t:Y\sqcup^{X}Z)}}{% \sum_{(t:Y\sqcup^{X}Z)}}}E(t)$ is equivalent the higher inductive type ${E^{\mathrm{tot}}}^{\prime}$ with the following generators:

•

a function $\mathsf{z}:\mathchoice{\sum_{a:Y+Z}\,}{\mathchoice{{\textstyle\sum_{(a:Y+Z)}}}% {\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}}{\mathchoice{{\textstyle\sum_% {(a:Y+Z)}}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}}{\mathchoice{{% \textstyle\sum_{(a:Y+Z)}}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}}C(a% )\to{E^{\mathrm{tot}}}^{\prime}$ ,
•

for each $x : X$ and $t:E_{Y}(j(x))$ , a path $\mathsf{z}({\mathsf{inl}}(j(x)),t)=\mathsf{z}({\mathsf{inr}}(k(x)),e_{C}(t)).$

Using the flattening lemma again or a direct computation, it is easy to see that $\mathchoice{\sum_{a:Y+Z}\,}{\mathchoice{{\textstyle\sum_{(a:Y+Z)}}}{\sum_{(a:Y% +Z)}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}}{\mathchoice{{\textstyle\sum_{(a:Y+Z)}}}% {\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}}{\mathchoice{{\textstyle\sum_% {(a:Y+Z)}}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}{\sum_{(a:Y+Z)}}}C(a)\simeq% \mathchoice{\sum_{y:Y}\,}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)}}{% \sum_{(y:Y)}}{\sum_{(y:Y)}}}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)% }}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y% :Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}E_{Y}(y)+\mathchoice{\sum_{z:Z}\,}{% \mathchoice{{\textstyle\sum_{(z:Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:Z)}% }}{\mathchoice{{\textstyle\sum_{(z:Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:% Z)}}}{\mathchoice{{\textstyle\sum_{(z:Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{% (z:Z)}}}E_{Z}(z)$ , hence ${E^{\mathrm{tot}}}^{\prime}$ is equivalent to the higher inductive type $E^{\mathrm{tot}}$ with the following generators:

•

a function ${\mathsf{inl}}:\mathchoice{\sum_{y:Y}\,}{\mathchoice{{\textstyle\sum_{(y:Y)}}}% {\sum_{(y:Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}{\mathchoice{{\textstyle\sum_{(y:Y)% }}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}{\mathchoice{{\textstyle\sum_{(y% :Y)}}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}E_{Y}(y)\to E^{\mathrm{tot}}$ ,
•

a function ${\mathsf{inr}}:\mathchoice{\sum_{z:Z}\,}{\mathchoice{{\textstyle\sum_{(z:Z)}}}% {\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}}{\mathchoice{{\textstyle\sum_{(z:Z)% }}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}}{\mathchoice{{\textstyle\sum_{(z% :Z)}}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}{\sum_{(z:Z)}}}E_{Z}(z)\to E^{\mathrm{tot}}$ ,
•

for each $(x,t):\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)}}}E_{Y}(j(x))$ a path $\mathsf{glue}(x,t):{\mathsf{inl}}(j(x),t)={\mathsf{inr}}(k(x),e_{X}(t)).$

Thus the total space of $E$ is the pushout of the total spaces of $E_{Y}$ and $E_{Z}$ , as required. ∎

Title	8.5.1 Fibrations over pushouts
\metatable