Closure properties of fibrations

Question

I am trying to prove the above theorem, I think I can do the backward direction. I wanted to be sure about the forward direction:

$(\implies)$ Suppose $F$ is a fibration. Then since fibrations are closed under composition, condition $(1)$ follows. To see that $F$ is a cartesian functor, consider a $Q$-cartesian morphism $\varphi \colon Z \to Y$ in $\mathbf{Y}$ over $P(f)$ where $f \colon X \to FY$ is $P$-cartesian over $P(f)$ such that $P(F(\varphi)) = Q(\varphi)=P(f)$. Since both maps are cartesian over $P(f)$, we have $f \cong F(\varphi)$. To show condition $(2)$, if we suppose $F_J \colon Y_J \to X_J$ is a fibration and $u \colon X_I \to X_J$ is a functor. The pullback of $F_J$ along $u$ is also a fibration. So $F_I$ is a fibration. Because $F$ is cartesian functor (from $(1)$), it follows that $u^* \colon Y_I \to Y_J$ is cartesian. Hence the square is a morphism in $\mathbf{Fib}$.

Answer 1

Your proof is nice, except for the first piece of $(2)$ where the lemma asks you to show that all $F_I$ are fibrations, but you begin by assuming that $F_J$ is. Rather, proceed as follows:

We wish to show that $F_I:{\bf Y}_I\to{\bf X}_I$ is a fibration for each $I\in{\bf Ob}_\mathcal{B}$. To this end, suppose we have an object $X\in{\bf Ob}_{{\bf Y}_I}$ and an arrow $u:X'\to F(X)\in{\bf Hom}_{{\bf X}_I}$. Since $F$ is a fibration by assumption, there exists an $F$-Cartesian arrow $f:A\to B\in{\bf Hom}_{\bf Y}$ with $F(f)=u$. We wish to show that $f\in{\bf Hom}_{{\bf Y}_I}$; recall that since $u\in{\bf Hom}_{{\bf X}_I}$ we have $P(u)=1_I$, thus $$P(F(f))=P(u)=1_I\implies f\in{\bf Hom}_{{\bf Y}_I}.$$

For bonus points prove all of this for Street fibrations, the 'correct' notion of fibration if you take the principle of equivalence seriously (or have questions about free will).