# Kerodon

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

Corollary 7.5.4.12. Let $\operatorname{\mathcal{C}}$ be a category and let $\overline{ \mathscr {F} }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be a functor. Let $\overline{ \mathscr {F} }^{\operatorname{op}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be the functor given on objects by $\overline{ \mathscr {F} }^{\operatorname{op}}(C) = \overline{\mathscr {F}}(C)^{\operatorname{op}}$. Then $\overline{\mathscr {F}}$ is a homotopy limit diagram if and only if $\overline{\mathscr {F}}^{\operatorname{op}}$ is a homotopy limit diagram.

Proof. For each object $C \in \operatorname{\mathcal{C}}^{\triangleleft }$, let $| \overline{\mathscr {F}}(C) |$ denote the geometric realization of the simplicial set $\overline{\mathscr {F}}(C)$ (Definition 1.1.8.1). Then the construction $C \mapsto \operatorname{Sing}_{\bullet }( | \overline{ \mathscr {F} }(C) | )$ determines a functor $\overline{\mathscr {G}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$, and the unit maps $\overline{ \mathscr {F} }(C) \rightarrow \operatorname{Sing}_{\bullet }( | \overline{ \mathscr {F}}(C) |)$ determine a levelwise weak homotopy equivlaence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$ (Theorem 3.5.4.1). By virtue of Corollary 7.5.4.11, it will suffice to show that the functor $\overline{\mathscr {G}}$ is a homotopy limit diagram if and only if $\overline{ \mathscr {G} }^{\operatorname{op}}$ is a homotopy limit diagram. This is clear, since the functors $\overline{ \mathscr {G} }$ and $\overline{ \mathscr {G} }^{\operatorname{op}}$ are isomorphic (see Example 1.3.2.5). $\square$