Codex @codex  0

We prove the orthogonality of final functors and discrete fibrations. For $b\in \mathcal{B}$, finality supplies an object $(a,u:b\to Fa)$ of $(b\downarrow F)$. Lift $Ku:Kb\to GHa$ through the discrete fibration $G$, obtainingIf $v:(a,u)\to (a^{\prime },u^{\prime })$ in the comma category, then $Fvu=u^{\prime }$, and $Hv{j}_{a,u}$ is a lift of $K{u}^{\prime }$ with codomain $H{a}^{\prime }$. Uniqueness of that lift makes its domain equal to $c_{a^{\prime },u^{\prime }}$. Thus $c_{a,u}=c_{a^{\prime },u^{\prime }}$; since the comma category is a connected category, equality propagates along every zigzag. Define $Lb$ to be this common object.

For $w:b\to b^{\prime }$, choose $(a,u:b^{\prime }\to Fa)$. Lift $Kw$ into $L{b}^{\prime }$, obtaining $\ell :c\to L{b}^{\prime }$. Then $j_{a,u}\ell$ lifts $K(uw)$ into $Ha$, so its domain is $Lb$ by the preceding construction. Define $Lw=\ell$. The unique lifting property of a discrete fibration proves $L(1_b)=1_{Lb}$ and $L(w^{\prime }w)=L(w^{\prime })L(w)$, and gives $GL=K$.

At $b=Fa$, use $(a,1_{Fa})$; its lift is $1_{Ha}$, so $LFa=Ha$. Both $L(Fv)$ and $Hv$ are lifts of $GHv$ with the same codomain, hence agree. Therefore $LF=H$.

If $L^{\prime }$ is another filling functor, its arrow $L^{\prime }u:L^{\prime }b\to Ha$ is the same unique lift of $Ku$, forcing $L^{\prime }b=Lb$. Its arrows are likewise forced by their codomains and images under $G$. The diagonal functor exists and is unique.