8.5.1 Fibrations over pushouts

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

Lemma 8.5.1.

Let $\mathrm{D}\mathrm{=}\mathrm{(}Y\stackrel{𝑗}{\mathrm{\leftarrow }}X\stackrel{𝑘}{\mathrm{\to }}Z\mathrm{)}$ be a span and assumethat we have

• Two fibrations $E_Y:Y\to 𝒰$ and $E_Z:Z\to 𝒰$.

• An equivalence $e_X$ between $E_Y\circ j:X\to 𝒰$ and $E_Z\circ k:X\to 𝒰$, i.e.

  $$e_X:\prod _{x:X}{E}_Y(j(x))\simeq E_Z(k(x)).$$

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

• For all $y:Y$, $E(\mathrm{𝗂𝗇𝗅}(y))\equiv E_Y(y)$.

• For all $z:Z$, $E(\mathrm{𝗂𝗇𝗋}(z))\equiv E_Z(z)$.

• For all $x:X$, $E\left(\mathrm{𝗀𝗅𝗎𝖾}(x)\right)=\mathrm{𝗎𝖺}(e_X(x))$ (note that both sides ofthe equation are paths in $𝒰$ from $E_Y(j(x))$ to $E_Z(k(x))$).

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

Proof.

We define $E$ by the recursion principle of the pushout $Y{\bigsqcup }^{X}Z$. Forthat, we need to specify the value of $E$ on elements of the form $\mathrm{𝗂𝗇𝗅}(y)$, $\mathrm{𝗂𝗇𝗋}(z)$and the action of $E$ on paths $\mathrm{𝗀𝗅𝗎𝖾}(x)$, so we can just choose the followingvalues:

$E(\mathrm{𝗂𝗇𝗅}(y))$$:\equiv E_Y(y),$

$E(\mathrm{𝗂𝗇𝗋}(z))$$:\equiv E_Z(z),$

$E\left(\mathrm{𝗀𝗅𝗎𝖾}(x)\right)$$\mathrm{𝗎𝖺}(e_X(x)).$

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

• $A:\equiv Y+Z$, $B:\equiv X$ and $f,g:B\to A$ are defined by$f(x):\equiv \mathrm{𝗂𝗇𝗅}(j(x))$, $g(x):\equiv \mathrm{𝗂𝗇𝗋}(k(x))$,

• the type family $C:A\to 𝒰$ is defined by

  $$C(\mathrm{𝗂𝗇𝗅}(y)):\equiv E_Y(y)\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}C(\mathrm{𝗂𝗇𝗋}(z)):\equiv E_Z(z),$$

• the family of equivalences $D:{\prod }_{(b:B)}C(f(b))\simeq C(g(b))$ is definedto be $e_X$.

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

Thus the flattening lemma tells us that ${\sum }_{(t:Y{\bigsqcup }^{X}Z)}E(t)$ is equivalentthe higher inductive type $E^{\mathrm{tot}}{}^{\prime }$ with the following generators:

• a function $𝗓:{\sum }_{(a:Y+Z)}C(a)\to E^{\mathrm{tot}}{}^{\prime }$,

• for each $x:X$ and $t:E_Y(j(x))$, a path$𝗓(\mathrm{𝗂𝗇𝗅}(j(x)),t)=𝗓(\mathrm{𝗂𝗇𝗋}(k(x)),e_C(t)).$

Using the flattening lemma again or a direct computation, it is easy to seethat ${\sum }_{(a:Y+Z)}C(a)\simeq {\sum }_{(y:Y)}{E}_Y(y)+{\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 $\mathrm{𝗂𝗇𝗅}:{\sum }_{(y:Y)}{E}_Y(y)\to E^{\mathrm{tot}}$,

• a function $\mathrm{𝗂𝗇𝗋}:{\sum }_{(z:Z)}{E}_Z(z)\to E^{\mathrm{tot}}$,

• for each $(x,t):{\sum }_{(x:X)}{E}_Y(j(x))$ a path$\mathrm{𝗀𝗅𝗎𝖾}(x,t):\mathrm{𝗂𝗇𝗅}(j(x),t)=\mathrm{𝗂𝗇𝗋}(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.∎