Finite families in an ∞-category

Construction 14.1.16 (Finite families). Let \(C\) be an \(\infty \)-category. There is a unique finite-product-preserving functor \[ C^{(-)}\colon \Fin \catop \to \Cat _{\infty } \] which sends the one-point set to \(C\); explicitly, it sends a finite set \(I\) to the \(\infty \)-category \(C^I\) of \(I\)-indexed families and a map \(f\colon I \to J\) to the restriction functor \(f^*\colon C^J \to C^I\). Equivalently, this functor is the right Kan extension of \(C\) from the one-point set. We write \[ q\colon \Fin (C) \to \Fin \] for its cartesian unstraightening. Thus objects of \(\Fin (C)\) are finite unordered tuples \(\{x_i\}_{i \in I}\), while morphisms \(\{x_i\}_{i \in I} \to \{y_j\}_{j \in J}\) are pairs \((f,(\phi _i)_{i \in I})\) consisting of a map \(f\colon I \to J\) and morphisms \(\phi _i\colon x_i \to y_{f(i)}\) in \(C\) for all \(i \in I\).