 Uniqueness of a final-discrete-fibration factorization

Two factorizations of one functor have a unique connecting functor in each direction, by the orthogonality of final functors and discrete fibrations. Their composites and the identity fill the same lifting square, so uniqueness makes both composites identities. The intermediate categories are therefore canonically isomorphic.