Orthogonality of final functors and discrete fibrations
= Orthogonality of final functors and discrete fibrations
Given a commutative square whose left functor is <final functor>[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.