I've been trying to learn some of the basic language of infinity-category theory (in the sense of Lurie), and in particular, to understand which basic statements in (1-)categories have analogues in the infinity-categorical setting. Specifically, I'm trying to understand how equivalences behave in infinity categories, motivated by the following question.

Vague Question:in an infinity-category $\mathcal C$, to what extent is it true that a quasi-inverse to a morphism $f$, if it exists, is unique up to a contractible space of choices?

Here is how I believe this question should be made precise. If we let $I$ denote the nerve of the undirected interval category (the category with two objects and exactly one morphism between each pair of objects), then there is an inclusion $\Delta^1\hookrightarrow I$ coming from the inclusion of the directed interval category in the undirected interval category. Thus we have a restriction map $$\mathcal C^I\rightarrow\mathcal C^{\Delta^1}$$ of simplicial sets (in fact a functor of infinity-categories which is a fibration for the Joyal model structure), where informally the left-hand side is the infinity-category of quasi-inverse pairs $(g,h)$ of morphisms in $\mathcal C$ (with a family of homotopies realising their quasi-inverseness), the right-hand side is the infinity-category of arrows in $\mathcal C$, and the functor takes a pair $(g,h)$ to its first component $g$.

Precise Question:if $f$ is a morphism in an infinity-category $\mathcal C$, is it true that the fibre of the map $\mathcal C^I\rightarrow\mathcal C^{\Delta^1}$ over the point $f$ of $\mathcal C^{\Delta^1}$ is either empty or a contractible Kan complex?

I am interested both in answers to the precise question and the vague questions above, especially if there are alternative precise formulations which make the answer clearer.

**Remark:**

The condition that $f$ admit a quasi-inverse should be be equivalent to the assertion that it be an isomorphism in the homotopy category of $\mathcal C$. This is asserted in this nlab page, and something similar in the language of topological categories is proved in the setting of topological categories in Proposition 1.2.4.1 of *Higher Topos Theory*.