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?



How to define the $\infty$-category of left fibrations?
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:



> 
> Consider three quasi-categories $C,D,E$ with functors $p: C\to E, q:D \to E$. Suppose $q: D\to E$ is a cocartesian fibration. In this situation, the quasi-category $Fun\_E(C,D)$ defined as a simplicial set by the (ordinary) pullback $Fun(C,D)\times\_{Fun(C,E)}\{p\}$ is equivalent to the homotopy pullback, $Fun(C,D)\times\_{Fun(C,E)}(Fun(C,E)^\simeq)\_{/p}$
> 
> 
> 


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)


