Solution (source code)

= Solution

Write the square as $GH=KF$, with $F:\mathcal A\to\mathcal B$ final and $G:\mathcal C\to\mathcal D$ a <discrete fibration>. For $b\in\mathcal B$, choose an object $(a,h:b\to Fa)$ of the nonempty <comma category> $(b\downarrow F)$. Lift $K(h):Kb\to GHa$ uniquely to an arrow
$$
\ell_h:c_h\longrightarrow Ha
$$
over $K(h)$, and tentatively put $L(b)=c_h$.

A morphism $(a,h)\to(a',h')$ in this <comma category> is an arrow $j:a\to a'$ with $F(j)h=h'$. The composite $H(j)\ell_h$ is a lift of $K(h')$ with codomain $Ha'$. Uniqueness of lifts gives $H(j)\ell_h=\ell_{h'}$, including equality of their source objects. Since the <comma category> is connected by zigzags, $c_h$ is independent of the choice. Thus $L(b)$ is well defined and $GL(b)=Kb$.

For $f:b\to b'$, take $(a',h':b'\to Fa')$. Lift $K(f)$ into $L(b')$, obtaining $t:c\to L(b')$. Composing with $\ell_{h'}$ gives a lift of $K(h'f)$ into $Ha'$, whose source must be $L(b)$. Hence $t:L(b)\to L(b')$. Set $L(f)=t$. Uniqueness of this lift makes the definition independent of the chosen comma object and proves $L(1_b)=1_{L(b)}$ and $L(gf)=L(g)L(f)$.

At $b=Fa$, choose $(a,1_{Fa})$. Its lift is $1_{Ha}$, so $L(Fa)=Ha$. For $j:a\to a'$, $Hj$ is the unique lift of $K(Fj)$ into $Ha'$, so $L(Fj)=Hj$. We have constructed the required <functor> with $LF=H$ and $GL=K$.

If $L'$ is another filler, $L'(h):L'b\to Ha$ must equal $\ell_h$ by unique lifting. Thus $L'b=L(b)$ for every object. Its arrows are then forced by unique lifting into those objects. Therefore
$$
\boxed{L\text{ exists and is unique}.}
$$
This proves the <orthogonality of final functors and discrete fibrations>.