Cocartesian fibrations and (un)straightening

An important notion in \(\infty \)-category theory is that of a cocartesian fibration. Roughly speaking, a cocartesian fibration is a functor \(p\colon E \to C\) whose fibers \(E_x := E \times _C \{x\}\) vary covariantly in \(x\), in the sense that for every morphism \(f\colon x \to y\) in \(C\) we obtain a cocartesian transport functor \(f_!\colon E_x \to E_y\). These functors are fully coherent in \(f\), in the sense that they assemble into a functor \(\Str (p)\colon C \to \Cat _{\infty }\), given on objects by sending \(x\) to \(E_x\) and on morphisms by sending \(f\) to \(f_!\). This provides a powerful way to construct functors into \(\Cat _{\infty }\), known as the straightening/unstraightening correspondence. For example, it will allow us to formally define the hom functor \(\Hom _C\colon C\catop \times C \to \An \) of an \(\infty \)-category \(C\).

Generated from the authoritative LaTeX source.