Uniqueness of a final-discrete-fibration factorization
= 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>.