8.5.1 Fibrations over pushouts

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

Lemma 8.5.1.

Let D=(Y𝑗X𝑘Z) be a span and assume that we have

  • Two fibrations EY:Y𝒰 and EZ:Z𝒰.

  • An equivalence eX between EYj:X𝒰 and EZk:X𝒰, i.e.


Then we can construct a fibration E:YXZU such that

  • For all y:Y, E(𝗂𝗇𝗅(y))EY(y).

  • For all z:Z, E(𝗂𝗇𝗋(z))EZ(z).

  • For all x:X, E(𝗀𝗅𝗎𝖾(x))=𝗎𝖺(eX(x)) (note that both sides of the equation are paths in 𝒰 from EY(j(x)) to EZ(k(x))).

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


We define E by the recursion principle of the pushout YXZ. For that, we need to specify the value of E on elements of the form 𝗂𝗇𝗅(y), 𝗂𝗇𝗋(z) and the action of E on paths 𝗀𝗅𝗎𝖾(x), so we can just choose the following values:

E(𝗂𝗇𝗅(y)) :EY(y),
E(𝗂𝗇𝗋(z)) :EZ(z),
E(𝗀𝗅𝗎𝖾(x)) \coloneqq𝗎𝖺(eX(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:Y+Z, B:X and f,g:BA are defined by f(x):𝗂𝗇𝗅(j(x)), g(x):𝗂𝗇𝗋(k(x)),

  • the type family C:A𝒰 is defined by

    C(𝗂𝗇𝗅(y)):EY(y)  and  C(𝗂𝗇𝗋(z)):EZ(z),
  • the family of equivalences D:(b:B)C(f(b))C(g(b)) is defined to be eX.

The base higher inductive type W in the flattening lemma is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the pushout YXZ and the type family P:YXZ𝒰 is equivalent to the E defined above.

Thus the flattening lemma tells us that (t:YXZ)E(t) is equivalent the higher inductive type Etot with the following generatorsPlanetmathPlanetmath:

  • a function 𝗓:(a:Y+Z)C(a)Etot,

  • for each x:X and t:EY(j(x)), a path 𝗓(𝗂𝗇𝗅(j(x)),t)=𝗓(𝗂𝗇𝗋(k(x)),eC(t)).

Using the flattening lemma again or a direct computation, it is easy to see that (a:Y+Z)C(a)(y:Y)EY(y)+(z:Z)EZ(z), hence Etot is equivalent to the higher inductive type Etot with the following generators:

  • a function 𝗂𝗇𝗅:(y:Y)EY(y)Etot,

  • a function 𝗂𝗇𝗋:(z:Z)EZ(z)Etot,

  • for each (x,t):(x:X)EY(j(x)) a path 𝗀𝗅𝗎𝖾(x,t):𝗂𝗇𝗅(j(x),t)=𝗂𝗇𝗋(k(x),eX(t)).

Thus the total space of E is the pushout of the total spaces of EY and EZ, as required. ∎

Title 8.5.1 Fibrations over pushouts