First, let F, G: \mathcal {K} \to \mathcal {C} be two pseudofunctors, and consider the category \operatorname {Nat}(F,G) of strong natural transformations F \Rightarrow G and modifications between these. We must prove that p is a local fibration, i.e that \operatorname {Nat}(F,G) \to \operatorname {Nat}(pF,pG) is a 1-fibration.

Thus let \alpha : F \Rightarrow G be a strong natural transformation, and let \Gamma : p(\alpha ) \to \beta ' be a modification, where \beta ': pF \Rightarrow pG is some other strong natural transformation. Then \Gamma consists in a family of 2-cells in \mathcal {D} \Gamma _X: p(\alpha )_X \Rightarrow \beta _X'. These are 2-cells p(\alpha _X) \to \beta '_X and so we can find a family of Cartesian lifts \alpha _X \to \beta _X (where this defines \beta _X)

The Cartesian-ness of the lift \alpha _X \to \beta _X suffices to generate the necessary naturality squares

DIAGRAM HERE

, and it is similarly not too hard to see that the equations hold. The equations for being a modification hold by construction, so that the lifted maps \alpha _X \to \beta _X assemble into a modification. The same argument will show that, given some other modification \gamma \to \alpha and a factorization over \beta ' in the base, it lifts and lifts uniquely to the total category.

Let us stop here to note that, if the hom-fibrations of \mathcal {C}(X,Y) \to \mathcal {D}(pX,pY) are discrete fibrations, then the lifts above will be unique, and hence the modification lifting \Gamma will be unique, and so also \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {C})(F,G) \to \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {D})(pF,pG) will be a discrete fibration. Since this is what it means to be fibred in 1-categories, this proves part 2 of the lemma.

Now if F: \mathcal {K} \to \mathcal {C} is a functor, and \alpha : G' \Rightarrow pF is a natural transformation, we must construct again a Cartesian lift. As before, since the uniqueness properties making something Cartesian can more or less be checked object-wise, the difficult part is verifying that the individual objects \alpha _X^*F(X) assemble into a pseudofunctor.

But once again, this can be done piecewise. Since the map \alpha _Y^*F(Y) \to F(Y) is Cartesian, given each f: X \to Y \in \mathcal {K}, there is an essentially unique filler in the below diagram:

which defines the action on morphisms and the naturality squares for the lift of \alpha , and one proceeds like this.