Kerodon

Proof. Set $\operatorname{\mathcal{C}}' = \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}})$ and $\operatorname{\mathcal{D}}' = \operatorname{Fun}(K,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{D}}) } \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}})$, so that $U$ induces an inner fibration $U': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}'$ (Proposition 4.1.4.1). We can then rewrite (7.5) as a lifting problem

Let $P$ be the partially ordered set of pairs $(A', g')$, where $A' \subseteq B$ is a simplicial subset containing $A$, and $g': A' \rightarrow \operatorname{\mathcal{C}}'$ is a morphism satisfying $g'|_{A} = g$ and $U' \circ g' = g_0|_{A'}$. The partially ordered set $P$ satisfies the hypotheses of Zorn's lemma and therefore contains a maximal element $(A_{\mathrm{max}}, g_{\mathrm{max}})$. To complete the proof, it will suffice to show that $A_{\mathrm{max}} = B$. Assume otherwise: then there exists some $n$-simplex $\sigma : \Delta ^ n \rightarrow B$ which is not contained in $A_{\mathrm{max}}$. Choose $n$ as small as possible, so that $\sigma $ carries the boundary $\operatorname{\partial \Delta }^ n$ into $A_{\mathrm{max}}$. Since every vertex of $A$ is contained in $B$, we must have $n > 0$. Moreover, it follows from $(\ast )$ together with Proposition 7.1.7.4 that the vertex $a = \sigma (0)$ is a $U'$-initial object of $\operatorname{\mathcal{C}}'$. Applying Corollary 7.1.5.17, we deduce that the lifting problem

has a solution, which contradicts the maximality of $(A_{\mathrm{max}}, g_{\mathrm{max}} )$. $\square$