Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Example 9.4.1.22. Suppose we are given a commutative diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [dr]_{ U } \ar [rr]^-{H} & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U} } \\ & \operatorname{\mathcal{C}}, & } \]

which exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise idempotent completion of $\operatorname{\mathcal{E}}$. Then, for any idempotent complete inner fibration $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$, precomposition with $H$ induces an equivalence of $\infty $-categories

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \rightarrow \operatorname{Fun}_{/ \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ). \]

This follows by combining Theorem 9.4.1.20 with Corollary 8.5.3.12.