Lemma 15.3.9. For every finite set \(I\), restriction along the functor \(I\hookrightarrow (\Fin _{/I})\catop \) given by \(i\mapsto (\{i\}\hookrightarrow I)\) induces an equivalence \[ \Fun ^{\times }((\Fin _{/I})\catop ,C)\iso C^I. \]
Proof. Regarding \(I\) as a discrete \(\infty \)-category, the description of finite families in Construction 14.1.16 gives a finite-coproduct-preserving equivalence \[ \Fin (I)\iso \Fin _{/I} \] which sends a finite family of elements of \(I\) to its indexing map to \(I\). The dual of Lemma 14.1.17 therefore identifies restriction to the singleton families with an equivalence \[ \Fun ^{\times }((\Fin _{/I})\catop ,C) \simeq \Fun (I,C) = C^I. \] Under this equivalence, a functor \(F\) corresponds to its values on the singleton inclusions, and one has \[ F(U\to I)\simeq \prod _{u\in U}F(\{u\}\to I).\qedhere \] □
Generated from the authoritative LaTeX source.