# On HTT's remark 2.4.1.9

Background
I have some difficulty to understand remark 2.4.1.9 in Lurie's HTT, which says a $$p$$-Cartesian edge is determined up to equivalence.
To be more precise, let $$p:X\to S$$ be an inner fibration of simplicial sets, let $$x$$ be a vertex of $$X$$, and let $$\bar{f}:\bar{y}\to p(x)$$ be an edge of $$S$$ ending at $$p(x)$$. If there are two $$p$$-Cartesian edges $$f:y\to x$$ and $$f':y'\to x$$ in $$X$$ with $$p(f)=p(f')=\bar{f}$$, then we have that $$f$$ and $$f'$$ are strong final objects of the $$\infty$$-category $$K\stackrel{\text{def}}{=}X_{/x} \times_{S{/p(x)}}\{\bar{f}\}$$, and thus they are equivalent $$K$$.
That's true. Since for a $$p$$-Cartesian edge $$f$$, $$q:X_{/f}\to X_{/x}\times_{S_{/p(x)}}S_{/p(f)}$$ is a trivial fibration, and $$K_{/\{f\}}\to K$$ is a pullback of $$q$$.

My Question:
But since Lurie's original words are "($$p$$-Cartesian edge) is therefore determined up to equivalence by $$\bar{f}$$ and $$x$$", I think we should conversely have that an object who is equivalent with a $$p$$-Cartesian edge is also a $$p$$-Cartesian edge. And he indeed utilized such a claim in the proof of Proposition 2.4.2.4 in HTT. However I cannot figure out a detailed proof. I hope someone can help me.

If you have a map $$g$$ in $$X_{/x}$$ from $$f$$ to $$f'$$, it is, by definition, a 2-simplex $$\sigma$$ of $$X$$, with faces $$f'$$, $$f$$, and $$\bar g$$, expressing that $$f = f' \circ \bar g$$.
If the map $$g$$ is an equivalence, then $$\bar g$$ is an equivalence (because $$\bar g$$ is the image of $$g$$ under the functor $$X_{/x} \to X$$). HTT 2.4.1.5 says that equivalences are $$p$$-Cartesian, so $$\bar g$$ is $$p$$-Cartesian. HTT 2.4.1.7 implies that composites of $$p$$-Cartesian edges are $$p$$-Cartesian, so if $$f'$$ is $$p$$-Cartesian, so is $$f$$. Applying the same to an inverse of $$g$$ gives the converse.
• Thanks for your answer. But to prove 2.4.1.5, which comes from, 1.2.4.3, we essentially use the condition of $\infty$-categories. Also, 2.4.1.7 only applies to an inner fibration between $\infty$-categories. Can we do it in general case? – Jiaqi FU Dec 2 '20 at 21:44
Take a look at Proposition 55.6 in Charles Rezk's notes Stuff about quasi-categories, (which is the formal meaning of Lurie's words). It says that fix an edge $$\bar{f}:\bar{y}\to p(x)$$ in $$S$$, the "space" of $$p$$-Cartesian lifts of $$\bar{f}$$ is contractible.