In his book Introduction to Infinity-Categories, Land in his Theorem 3.3.16 asserts an equivalence of $\infty$-categories where one of the categories $\mathrm{LFib}(\mathcal C)$ is the full subcategory of $(\mathrm{Cat}_\infty)_{/\mathcal C}$ on vertices that are left fibrations $?\to\mathcal C$ ($\mathcal C$ some $\infty$-category). My understanding of this material is that he is following Riehl & Verity’s 2018 article The comprehension construction. There, in Notation 6.1.12, is defined a category $\mathrm{coCart}(\mathrm{qCat})_{/\mathcal C}$, and my understanding is that Land’s $\mathrm{LFib}(\mathcal C)$ should be the full subcategory of $\mathrm{coCart}(\mathrm{qCat})_{/\mathcal C}$ on vertices which are left fibrations with target $\mathcal C$. The definition of $\mathrm{coCart}(\mathrm{qCat})_{/\mathcal C}$ makes use of the slice $\infty$-cosmos defined in Riehl-Verity’s Elements, Proposition 1.2.22 (here our $\infty$-cosmos is $\mathrm{qCat}$). Per that definition, it seems to me that morphisms between left fibrations $h:\mathcal E\to\mathcal C$ and $f:\mathcal F\to\mathcal C$ in $\mathrm{coCart}(\mathrm{qCat})_{/\mathcal C}$ are simply functors $\mathcal E\to\mathcal F$ over $\mathcal C$. But 1-simplices in $(\mathrm{Cat}_\infty)_{/\mathcal C}$ are the data of a morphism $g:\mathcal E\to\mathcal F$ and a 1-simplex in $\operatorname{Fun}(\mathcal E,\mathcal C)$ between $fg$ and $h$ which is an equivalence in $\operatorname{Fun}(\mathcal E,\mathcal C)$. So these don’t seem like the same categories to me. Can someone familiar with these sources help me reconcile these two definitions?
Infinity-Category – Defining Left Fibrations
higher-category-theoryinfinity-categories
Best Answer
First let me point out a small typo : it should be functors over $\mathcal C$ which send cocartesian edges to cocartesian edges (this doesn't matter for left fibrations, but for cocartesian fibrations it does).
For your main point, you are right that they are different quasi-categories: the simplicial sets are not isomorphic; but they're the same $\infty$-category, that is, the obvious forgetful functor from one to the other (so the one that uses the trivial $1$-simplex) is a categorical equivalence.
The fact that it is essentially surjective is obvious (the objects are the same), so the point is really about mapping spaces. But this is really a statement about pullbacks, namely the following:
Note that the first one is the category of those functors $f :C\to D$ that are strictly over $E$, that is, with $q\circ f = p$, whereas $0$-simplices in the latter are a pair $(f, \sigma)$ where $f : C\to D$ is a functor and $\sigma: q\circ f \to p$ is an equivalence, and you can check that in fact it is what you're thinking of.
The reason for this equivalence is that $Fun(C,D)\to Fun(C,E)$ is also a cocartesian fibration, so in particular a fibration in the Joyal model structure, and so pull-back along it preserves weak equivalences. It then suffices to observe that the inclusion $\{p\}\to (Fun(C,E)^\simeq)_{/p}$ is an equivalence, because $Fun(C,E)^\simeq$ is a Kan complex.
The idea is that because $D\to E$ is a cocartesian fibration, you have "enough room" to "strictify" any equivalence $q\circ f\simeq p$ to an actual equality $q\circ f = p$ up to changing $f$.
(note that the latter, the one with $q\circ f\simeq p$, is the one that you would want to have as an $\infty$-category, because $=$ is too strict a notion. It just happens that in this case you can actually strictify)