Pullback of a section of a trivial fibration along a fibration Assume we have a category of fibrant objects and a pullback square in it, where both vertical maps are fibrations and the lower horizontal map is a weak equivalence, call it $i$. Assume further that $i$ is a section of a trivial fibration $\pi$.
I once saw the claim that the pullback of $\pi$ which is again a trivial fibration exhibits the upper horizontal map in my original square as the section of this trivial fibration or in other words: the pullback of a section of a trivial fibration along a fibration is again a section of a trivial fibration. Does somebody know the proof for this?
Sorry for the unhandy text but I cant use tikzcd here which I usually use for my diagrams.
 A: Suppose $i:X\rightarrow Y$ is a section of the trivial fibration $p:Y\overset{\sim}{\twoheadrightarrow} X$. Suppose that $f:X'\twoheadrightarrow X$ is a fibration. Consider the pullback $Y'$ of $p$ and $f$ as in
$$\begin{array}{ccc}
Y' &\overset{\sim}{\twoheadrightarrow}& X'\\
g\downarrow && \downarrow f\\
Y &\overset{\sim}{\underset{p}{\twoheadrightarrow}}& X
\end{array}$$
where the top arrow is a trivial fibration as pullback of a trivial fibration along a fibration.
The commutative square given by two parallel horizontal identities and the two vertical morphisms being $f$ gives rise to a commutative diagram
$$\tag{$\ast$}\begin{array}{ccccc}
X' &\underset{j}{\rightarrow} & Y' & \overset{\sim}{\underset{q}\twoheadrightarrow} & X'\\
f\downarrow &&g\downarrow&&f\downarrow\\
X &\underset{i}{\rightarrow} & Y & \overset{\sim}{\underset{p}\twoheadrightarrow}&X
\end{array}$$
in which the top and bottom composites are the identity. Note since the outer and right square are pullback squares, so is the left square. But this shows that the pullback of a section of a trivial fibration along a fibration is a section of a trivial fibration.
Note that in this argument it is essential to know that the morphism $g$ is given by the pullback of $f$ along $p$. If you only start with a pullback square
$$\begin{array}{ccc}
X' & \overset{j'}\rightarrow & Y'\\
f\downarrow && \downarrow g\\
X & \underset{i}\rightarrow & Y
\end{array}$$
it is not clear, whether $g$ is the pullback of $f$ along $p$. If this is is not the case, then $j'$ need not be a section of a trivial fibration, since it need not even be a split monomorphism (as a counterexample to the letter claim any two nonempty subsets with empty intersection will do). But if $g$ is the pullback of $f$ along $p$ we get a commutative diagram
$$\tag{$\ast\ast$}\begin{array}{ccccc}
X' &\underset{j'}{\rightarrow} & Y' & \overset{\sim}{\underset{q}\twoheadrightarrow} & X'\\
f\downarrow &&g\downarrow&&f\downarrow\\
X &\underset{i}{\rightarrow} & Y & \overset{\sim}{\underset{p}\twoheadrightarrow}&X
\end{array}$$
by pasting the two given pullback squares. Since both the left square in $(\ast)$ and the left square in $(\ast\ast)$ are pullback squares of the diagram $X \overset{i}\rightarrow Y \overset{g}\leftarrow Y'$ there exists a unique isomorphism $x:X'\cong X'$ induced from the pullbacks, which in particular satisfies $jx=j'$. But then $qj' = qjx=x$ implies $x^{-1}qj'=1_{X'}$ and thus shows that $j'$ is a section of the trivial fibration $x^{-1}q$.
