Naturality of straightening

Remark 23.2.11. In Theorem 23.2.1 we only formulated a ‘morphismwise’ version of functoriality of the straightening equivalences. Let us remark on how to formulate a fully functorial version.

For this, we will need to assume the existence of an even bigger universe \(\widehat {\Cat }_{\infty }\) of large \(\infty \)-categories, and assume that \(\Cat _{\infty }\) is an object of \(\widehat {\Cat }_{\infty }\), cf. Remark 1.8.1. Applying cartesian straightening to the cartesian fibration \(t\colon \Ar (\Cat _{\infty }) \to \Cat _{\infty }\) results in a contravariant functor \[ \Cat _{\infty }\catop \to \widehat {\Cat }_{\infty }, \quad C \mapsto (\Cat _{\infty })_{/C}, \quad (F\colon C \to D) \mapsto (F^*\colon (\Cat _{\infty })_{/D} \to (\Cat _{\infty })_{/C}). \] Since cocartesian fibrations are closed under pullback, this restricts to a functor \[ \Cocart (-)\colon \Cat _{\infty }\catop \to \widehat {\Cat }_{\infty }. \] Similarly, the assignment \(C \mapsto \Fun (C,\Cat _{\infty })\) defines a functor \[ \Fun (-,\Cat _{\infty }) \colon \Cat _{\infty }\catop \to \widehat {\Cat }_{\infty }, \] where functoriality is given by precomposition. The fully coherent version of the straightening equivalence would now ask for a natural equivalence \[ \Str ^{\cc }\colon \Cocart (-) \iso \Fun (-,\Cat _{\infty }) \] of functors \(\Cat _{\infty }\catop \to \widehat {\Cat }_{\infty }\).