Uniqueness of quasi-inverses in infinity categories

Question

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.

Answer 1

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.

Answer 2

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}$.