# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Remark 5.1.3.8 (Uniqueness of Locally Cartesian Lifts). Let $q: X \rightarrow S$ be an inner fibration of simplicial sets and let $g: y \rightarrow z$ be a locally $q$-cartesian edge of $X$. Suppose that $h: x \rightarrow z$ is another edge of $X$ satisfying $q(h) = q(g)$. Set $s = q(x) = q(y)$, and let $X_{s} = \{ s\} \times _{S} X$ denote the fiber of $q$ over the vertex $s$. Our assumption that $g$ is $q$-cartesian then guarantees that we can choose a $2$-simplex $\sigma$ of $X$ satisfying

$d_0(\sigma ) = g \quad \quad d_1(\sigma ) = h \quad \quad q(\sigma ) = s_0( q(g) ),$

which we display informally as a diagram

$\xymatrix@R =50pt@C=50pt{ & y \ar [dr]^{g} & \\ x \ar [ur]^{f} \ar [rr]^{h} & & z; }$

here $f = d_2(\sigma )$ is a morphism in the $\infty$-category $X_{s}$. In this case, the following conditions are equivalent:

$(1)$

The morphism $f$ is an isomorphism in the $\infty$-category $X_{s}$.

$(2)$

The morphism $h$ is locally $q$-cartesian.

To see this, we can replace $q$ by the projection map $\Delta ^1 \times _{S} X \rightarrow \Delta ^1$, and thereby reduce to the case where $g$ and $h$ are both lifts of the unique nondegenerate edge of $S = \Delta ^1$. In this case, the morphism $g$ is $q$-cartesian, and $(1)$ is equivalent to the assertion that $f$ is locally $q$-cartesian (Example 5.1.3.6). The equivalence of $(1)$ and $(2)$ is now a special case of Proposition 5.1.3.7.