Kerodon

Proof. Using Proposition 9.4.6.24 (or Exercise 9.4.6.25), we can choose a flat inner fibration $U': \operatorname{\mathcal{E}}' \rightarrow \Delta ^2$ and an isomorphism $F_0: \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{E}}' \xrightarrow {\sim } \Lambda ^{2}_{1} \times _{ \Delta ^2 } \operatorname{\mathcal{E}}$ of simplicial sets over $\Lambda ^{2}_{1}$. Since the inclusion map $\Lambda ^{2}_{1} \times _{ \Delta ^2 } \operatorname{\mathcal{E}}' \hookrightarrow \operatorname{\mathcal{E}}'$ is a categorical equivalence of simplicial sets, we can extend $F_0$ to a functor of $\infty $-categories $F: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ (which automatically satisfies $U \circ F = U'$). To prove that $U$ is flat, it will suffice to show that $F$ is an equivalence of inner fibrations over $\Delta ^2$ (Remark 9.4.6.3).

By construction, $F$ is bijective on objects. By virtue of Corollary 5.1.7.10, we are reduced to showing that $F$ is fully faithful: that is, for every pair of objects $X',Y' \in \operatorname{\mathcal{E}}'$ having images $X = F(X')$ and $Y = F(Y')$, the morphism $\overline{F}$ induces a homotopy equivalence of Kan complexes $\operatorname{Hom}_{\operatorname{\mathcal{E}}'}( X', Y' ) \rightarrow \operatorname{Hom}_{ \operatorname{\mathcal{E}}}( X, Y)$. We may assume that $U(X) = 0$ (otherwise, the result follows immediately from the fact that $F$ is an isomorphism). Choose an uncountable regular cardinal $\kappa $ such that $\operatorname{\mathcal{E}}$ and $\operatorname{\mathcal{E}}'$ are essentially $\kappa $-small, let $h_{X}: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be the functor represented by $X$, and define $h_{X'}: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ similarly. The functor $F$ then induces a natural transformation $\alpha : h_{X'} \rightarrow h_{X} \circ F$, and we wish to show that $\alpha $ is an isomorphism. Let $\operatorname{\mathcal{E}}'_{ \leq 1 }$ denote the full subcategory of $\operatorname{\mathcal{E}}'$ spanned by those objects $Y$ satisfying $U(Y) \leq 1$, and define $\operatorname{\mathcal{E}}'_{1}$ and $\operatorname{\mathcal{E}}'_{\geq 1}$ similarly. Since $F_0$ is an isomorphism, the natural transformation $\alpha $ is an isomorphism when restricted to $\operatorname{\mathcal{E}}'_{\leq 1}$. It will therefore suffice to show that $\alpha $ is also an isomorphism when restricted $\operatorname{\mathcal{E}}'_{\geq 1}$. Our assumption (and the fact that $F_0$ is an isomorphism) guarantees that $(h_{X} \circ F)|_{ \operatorname{\mathcal{E}}'_{\geq 1} }$ is left Kan extended from $\operatorname{\mathcal{E}}'_{1}$. Since $U'$ is flat, Lemma 9.4.7.2 guarantees that the functor $h_{X'}|_{ \operatorname{\mathcal{E}}'_{\geq 1} }$ is also left Kan extended from $\operatorname{\mathcal{E}}'_{1}$. The desired result now follows from the fact that $\alpha $ is an isomorphism when restricted to $\operatorname{\mathcal{E}}'_{1}$. $\square$