Uniqueness of quasi-inverses in infinity categories

If $C$ is a category, its core is the subgroupoid consisting of the isomorphisms of $C$. This generalizes; if $\mathcal{C}$ is an $\infty$-category, we define its core is the $\infty$-subgroupoid consisting only of equivalences.

If $\mathcal{C}$ is a quasi-category, define $\mathrm{Core}(\mathcal{C})$ by the following pullback of simplicial sets:

$$ \require{AMScd} \begin{CD} \mathrm{Core}(\mathcal{C}) @>>> \mathcal{C} \\ @VVV @VVV \\ \mathbf{N}(\mathrm{Core}(\mathrm{h}\mathcal{C})) @>>> \mathbf{N}(\mathrm{h}\mathcal{C}) \end{CD} $$ The bottom horizontal map is an inner fibration because it is a functor between (nerves of) categories (introduction to HTT section 2.3). I think you can show the right vertical map is an inner fibration as well. Therefore, $\mathrm{Core}(\mathcal{C})$ is a quasi-category. (and furthermore, this diagram computes a pullback in the $\infty$-category of $\infty$-categories)

HTT propositions 1.2.5.1 and 1.2.5.3 together imply that $\mathrm{Core}(\mathcal{C})$ is the maximal Kan subcomplex of $\mathcal{C}$. And by construction, we can see a morphism of $\mathcal{C}$ is in $\mathrm{Core}(\mathcal{C})$ if and only if it is an isomorphism in the homotopy category.

(the remarks following the proof of 1.2.5.3 state this construction is actually right adjoint to the inclusion $\mathbf{Kan} \to \mathbf{QuasiCat}$)

Since $\Delta^1 \to I$ is a Kan equivalence, it follows that there is an equivalence of $\infty$-groupoids $$ \mathrm{Core}(\mathcal{C})^I \to \mathrm{Core}(\mathcal{C})^{\Delta^1} $$ and the objects of $\mathrm{Core}(\mathcal{C})^{\Delta^1} \subseteq \mathcal{C}^{\Delta^1}$ are precisely functors mapping the arrow of $\Delta^1$ to an isomorphism of $\mathrm{h}\mathcal{C}$.

A possibly simpler way of proving what you are after is using marked simplicial set.

Recall that marked simplicial sets are pairs $(X,S)$ where $X$ is a simplicial set and $S\subseteq X_1$ is a set of 1-simplices of $X$ containing all degenerate 1-simplices. If $X$ is a simplicial set we will denote the minimal and maximal marking by $X^\flat$ and $X^\sharp$ respectively

If $X,Y$ are two marked simplicial sets, we can form additional simplicial sets $\mathrm{Map}^\flat(X,Y)$ and $\mathrm{Map}^\sharp(X,Y)$ by $$ \mathrm{Hom}_{\mathrm{sSet}}(K,\mathrm{Map}^\flat(X,Y))=\mathrm{Hom}_{\mathrm{sSet}^+}(K^\flat\times X,Y)\,,$$ $$ \mathrm{Hom}_{\mathrm{sSet}}(K,\mathrm{Map}^\sharp(X,Y))=\mathrm{Hom}_{\mathrm{sSet}^+}(K^\sharp\times X,Y)\,.$$

In HTT.3.1.3.7 a simplicial model structure is constructed on the category of marked simplicial sets such that the fibrant objects are precisely the $\infty$-categories with the equivalences marked.

The important part here will be that

• For any anodyne morphism of simplicial sets $A\to B$ the map $A^\sharp\to B^\sharp$ is a marked trivial cofibration. This is because of the definition of marked trivial cofibration (HTT.3.1.3.3) and the fact that for any simplicial set $A$ and every $\infty$-category $C$ $$ \mathrm{Map}^\sharp(A^\sharp,C)=\mathrm{Map}(A,\mathrm{Core}(C))$$

• If $f:X\to Y$ is a marked trivial cofibration and $C$ is a fibrant object (i.e. an $\infty$-category with the equivalences marked), then the map $$f^*:\mathrm{Map}^\flat(B,C)\to \mathrm{Map}^\flat(A,C)$$ is a trivial fibration (HTT.3.1.3.3)

Then we can factorize the arrow you want to study as $$C^J=\mathrm{Map}^\flat(J^\sharp,C)\to \mathrm{Map}^\flat((\Delta^1)^\sharp, C)\to \mathrm{Map}^\flat((\Delta^1)^\flat,C)=C^{\Delta^1}$$ The first arrow is a trivial fibration and the second is precisely the inclusion of the subcategory of $C^{\Delta^1}$ spanned by the equivalences.