Kerodon

Proof. Let $\operatorname{Fun}^{\mathrm{rep}}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})$ denote the full subcategory of $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})$ spanned by the representable functors. By virtue of Theorem 8.3.3.13, the construction $Y \mapsto \operatorname{Hom}_{\operatorname{\mathcal{C}}}( -, Y)$ determines an equivalence of $\infty $-categories $h^{\bullet }: \operatorname{\mathcal{C}}\rightarrow \operatorname{Fun}^{\mathrm{rep}}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})$. It follows that postcomposition with $h^{\bullet }$ induces an equivalence of $\infty $-categories

which is a restatement of Proposition 8.3.4.1. $\square$

Proof. Choose a realization of $\mathscr {K}$ as the covariant transport representation of a coupling of $\infty $-categories $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ (see Remark 8.3.2.5). By virtue of Remark 8.3.4.6, the coupling $\lambda $ is representable by the functor $G$. By virtue of Theorem 8.2.5.1, a functor $F: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{C}}_{+}$ is left adjoint to $G$ if and only if it corepresents the coupling $\lambda $. Invoking Remark 8.3.4.6 again, we see that this is equivalent to the requirement that $F$ corepresents the profunctor $\mathscr {K}$. $\square$

Proof. By virtue of Remarks 8.3.4.6 and 8.3.4.12, this follows by applying Proposition 8.2.4.3 to the coupling

Proof. By virtue of Remark 8.3.4.12, this is a special case of Proposition 8.2.4.9. $\square$

Proof. Let $\operatorname{\mathcal{E}}$ denote the oriented fiber product $\{ \Delta ^0 \} \operatorname{\vec{\times }}_{\operatorname{\mathcal{S}}} ( \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{D}})$ and let $\mu : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{D}}$ be the projection onto the second factor, so that we have a tautological natural transformation $\widetilde{\beta }: \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {K} \circ \mu $. It follows from Proposition 7.6.2.15 that $\widetilde{\beta }$ exhibits $\mathscr {K}$ as a left Kan extension of $\underline{\Delta ^0}_{\operatorname{\mathcal{E}}}$ along $\mu $. The natural transformation $\beta $ then determines a functor $T: \operatorname{Tw}( \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{E}}$ such that precomposition with $T$ carries $\widetilde{\beta }$ to $\beta $. By the transitivity of the formation of of Kan extensions (Proposition 7.3.7.18), we are reduced to showing that the identity transformation $\operatorname{id}: \underline{ \Delta ^0}_{ \operatorname{Tw}( \operatorname{\mathcal{D}}) } \rightarrow \underline{ \Delta ^{0} }_{\operatorname{\mathcal{E}}} \circ T$ exhibits $\underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}}$ as a left Kan extension of $\underline{ \operatorname{Tw}( \operatorname{\mathcal{D}}) }$ along $T$. This is a special case of Remark 7.6.2.12, since the functor $T$ is left cofinal (Proposition 8.3.4.18). $\square$

Proof. Combine Propositions 8.3.4.19 and 7.3.6.1. $\square$

Proof. Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $K \hookrightarrow \operatorname{\mathcal{K}}$, where $\operatorname{\mathcal{K}}$ is an $\infty $-category. Extend $G$ to a functor $\overline{G}: \operatorname{\mathcal{K}}\rightarrow \operatorname{\mathcal{C}}$. Since the restriction map $\operatorname{Fun}( \operatorname{\mathcal{K}}, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$ is a trivial Kan fibration (Proposition 1.4.7.6), we can replace $K$ by $\operatorname{\mathcal{K}}$ (and $G$ by $\overline{G}$) and thereby reduce to proving Corollary 8.3.4.22 in the special case where $K = \operatorname{\mathcal{K}}$ is an $\infty $-category.

Let $w: F \rightarrow F'$ be a morphism in $\operatorname{Fun}(\operatorname{\mathcal{K}}, \operatorname{\mathcal{C}})$ which belongs to $\widetilde{W}$; we wish to show that precomposition with $w$ induces a homotopy equivalence of Kan complexes $\theta : \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{K}}, \operatorname{\mathcal{C}}) }(F',G) \xrightarrow { \circ [w] } \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{K}}, \operatorname{\mathcal{C}}) }( F, G )$. Let $\mathscr {H}: \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be a $\operatorname{Hom}$-functor for $\operatorname{\mathcal{C}}$, let $U: \operatorname{Tw}(\operatorname{\mathcal{K}}) \rightarrow \operatorname{\mathcal{S}}$ be the functor given by the composition

and define $U': \operatorname{Tw}(\operatorname{\mathcal{K}}) \rightarrow \operatorname{\mathcal{S}}$ similarly. The morphism $w$ induces a natural transformation $\overline{w}: U' \rightarrow U$, which carries each object $(f: X \rightarrow Y)$ of $\operatorname{Tw}(\operatorname{\mathcal{K}})$ to the morphism of Kan complexes

given by precomposition with the morphism $w_{X}: F'(X) \rightarrow F(X)$ of $\operatorname{\mathcal{C}}$. Since $w_{X}$ belongs to $W$ and the object $G(Y) \in \operatorname{\mathcal{C}}$ is $W$-local, it follows that $\overline{w}_{f}$ is a homotopy equivalence. Applying Theorem 4.4.4.4, we see that $\overline{w}$ is an isomorphism (in the functor $\infty $-category $\operatorname{Fun}( \operatorname{Tw}(\operatorname{\mathcal{K}}), \operatorname{\mathcal{S}})$). We conclude by observing that Example 8.3.4.21 supplies an identification of $\theta $ with the image of $\overline{w}$ under the limit functor $\varprojlim : \operatorname{Fun}( \operatorname{Tw}(\operatorname{\mathcal{K}}), \operatorname{\mathcal{S}}) \rightarrow \operatorname{\mathcal{S}}$. $\square$