 Orthogonality of final functors and discrete fibrations

Given a commutative square whose left functor is final and whose right functor is a discrete fibration, there is a unique diagonal functor filling the square. To construct its value on an object, choose an object of the relevant connected comma category and lift the resulting arrow; uniqueness of lifts makes the answer constant over that connected category.