Fix \(x\in E\) and \(u,v\in {\mathopen {}\left [C\right ]\mathclose {}}_{x}\), we must exhibit a terminal object to the (total) category \(\widetilde {\mathbf {H}_{{\mathopen {}\left [C\right ]\mathclose {}}_{x}}(u,v)}\) of “hom candidates”
We define \(\overline {p}:{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}{u}\xrightarrow [p]{} u\in {\mathopen {}\left [C\right ]\mathclose {}}_{{\mathopen {}\left [u,v\right ]\mathclose {}}}\) to be
the cartesian lift of \(u\in {\mathopen {}\left [C\right ]\mathclose {}}_{x}\) along \(p:{\mathopen {}\left [u,v\right ]\mathclose {}}\to x\):
We need to define a displayed evaluation map
\(\epsilon : {\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\xrightarrow [p]{} v\); unraveling the definition of a displayed
morphism in the externalization of \(C\), we choose the following diagram:
Putting all this together, we assert that the terminal object of
\(\widetilde {\mathbf {H}_{{\mathopen {}\left [C\right ]\mathclose {}}_{x}}(u,v)}\) is the following span in \({\mathopen {}\left [C\right ]\mathclose {}}\):
Fixing another such candidate hom span \({\mathopen {}\left \{u \leftarrow \bar {h}\rightarrow v\right \}\mathclose {}}\in \widetilde {\mathbf {H}_{{\mathopen {}\left [C\right ]\mathclose {}}_{x}}(u,v)}\), we must exhibit
First we note that the evaluation map \(\epsilon _{h} : \bar {h}\to v\) amounts
to an internal morphism \(h\to C_{1}\) satisfying the appropriate
compatibility conditions. Therefore we may define the base \(\alpha :h\to {\mathopen {}\left [u,v\right ]\mathclose {}}\) of
the universal map using the universal property of the pullback that defines \({\mathopen {}\left [u,v\right ]\mathclose {}}\):
The morphism \(\alpha :h\to {\mathopen {}\left [u,v\right ]\mathclose {}}\) defined above is the unique map in \(E\)
satisfying the conditions required of the base for \(\bar \alpha \); therefore, it
suffices to show that there exists a cartesian morphism
\(\bar \alpha :\bar {h}\xrightarrow [\alpha ]{}{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\) since it will be unique if it
exists. We define \(\bar \alpha \) using the universal property of the cartesian lift:
That \(\bar {\alpha }:\bar {h}\xrightarrow [\alpha ]{}{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\) is cartesian follows from the generalized pullback lemma for cartesian morphisms