Are discrete fibrations closed under pullback? Let $P:E\to B$ be a discrete fibration of categories. Let $F:A\to B$ be a functor. Is the (strict) pullback $F^*P:A\times_B E \to A$ still a discrete fibration?
Also, is there a reference where this is explained in detail? Note that I want discrete fibrations in particular.
 A: Yes, $F^*P$ is a discrete fibration. I don't know of a reference, but it's straightforward to check explicitly.
Explicitly, the objects of $A \times_B E$ are pairs $(a \in A, e \in E)$ such that $F(a) = P(e)$, and $F^*P((a, e)) = a$. Consider a morphism $a' \to F^*P((a, e))$ in $A$, i.e. a morphism $a' \to a$. This is sent to $F(a') \to F(a)$ in $B$. We have that $F(a) = P(e)$, so, because $P$ is a discrete fibration, there is a unique morphism $e' \to e$ in $E$ such that $P(e' \to e) = F(a') \to F(a)$. Therefore, $P(e') = F(a')$ and so $(a', e') \in A \times_B E$, along with the morphism $(a', e') \to (a, e)$. This morphism is mapped under $F^*P$ to $a' \to a$ and is therefore a lifting of $a' \to a$. It remains to show that this lifting $(a', e') \to (a, e)$ in $A \times_B E$ is unique. As previously noted, the choice of $e' \to e$ in the lifting is unique, because $P$ is a discrete fibration; the choice of $a' \to a$ in the lifting is unique, because $F^*P$ is a projection. Therefore $F^*P$ is a discrete fibration.
