@CharlesRezk what does it mean? i seem to remember something like... if you pull back along the inclusion of an interval, it becomes Cartesian, or something?
That's the definition. But you can actually say it the following way: an edge $f$ is locally $p$-Cartesian if there exists a pullback square $q\Rightarrow p$ such that $f$ is the image of a $q$-Cartesian edge. In other words, locally Cartesian edges are the smallest class containing Cartesian edges which is "local", i.e., detected by taking pullbacks.
Ever since I read the definition of locally cartesian fibration over an $\infty$-category $\mathcal{C}$, I wanted to think of it as an unstraightning of a functor to some kind of $(\infty,\infty)$-category of $\infty$-categories $\mathcal{C} \to Cat_{(\infty,\infty)}$. Was anything of the sort ever done?
@SaalHardali By analogy with the classical case, locally cartesian fibrations over C should be equivalent to normal lax functors from C^op to the (infinity,2)-category of infinity-categories. I don't know if this has been proved.
I thought I recalled a discussion of the "straightened version" of locally cartesian fibrations in Clark and Jay's note but I can't find it in there now.
