= Solution
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$, obtaining
$$
j_{a,u}:c_{a,u}\longrightarrow Ha,\qquad Gj_{a,u}=Ku,\qquad Gc_{a,u}=Kb.
$$
If $v:(a,u)\to(a',u')$ in the <comma category>, then $Fv\,u=u'$, and $Hv\,j_{a,u}$ is a lift of $Ku'$ with codomain $Ha'$. Uniqueness of that lift makes its domain equal to $c_{a',u'}$. Thus $c_{a,u}=c_{a',u'}$; 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'$, choose $(a,u:b'\to Fa)$. Lift $Kw$ into $Lb'$, obtaining $\ell:c\to Lb'$. 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'w)=L(w')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'$ is another filling <functor>, its arrow $L'u:L'b\to Ha$ is the same unique lift of $Ku$, forcing $L'b=Lb$. Its arrows are likewise forced by their codomains and images under $G$. \b[The diagonal functor exists and is unique.]
Back to article page
