Proposition 4.4.5.1. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty $-categories, let $B$ be a simplicial set, and let $A \subseteq B$ be a simplicial subset. Then the restriction map
\[ F': \operatorname{Fun}(B, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}}) \]
is an isofibration of $\infty $-categories.
Proof of Proposition 4.4.5.1.
Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty $-categories, let $B$ be a simplicial set, and let $A \subseteq B$ be a simplicial subset. We wish to show that the restriction map
\[ F': \operatorname{Fun}(B, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}}) \]
is an isofibration of $\infty $-categories. We first note that the projection map
\[ \operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{C}}) \]
is a pullback of the inner fibration $\operatorname{Fun}(B, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{D}})$ (see Corollary 4.1.4.2). Since $\operatorname{Fun}(A, \operatorname{\mathcal{C}})$ is an $\infty $-category (Theorem 1.5.3.7), it follows that $\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ is also an $\infty $-category (Remark 4.1.1.9). It follows from Proposition 4.1.4.1 that $F'$ is an inner fibration. It will therefore suffice to show that, for every object $Y \in \operatorname{Fun}(B,\operatorname{\mathcal{C}})$, every isomorphism $u: X \rightarrow F'(Y)$ in the $\infty $-category $\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ can be lifted to an isomorphism $\overline{u}: \overline{X} \rightarrow Y$ in the $\infty $-category $\operatorname{Fun}(B, \operatorname{\mathcal{C}})$. This follows immediately from Corollary 4.4.5.9.
$\square$