Why are finite cell complexes also finite as infinity-categories?

Question

A quasicategory ($\infty$-category) $\mathcal{C}$ is finite if there is a finite simplicial set $K$ and a categorical equivalence $K\rightarrow\mathcal{C}$.

On the other hand, a Kan complex (space) $X$ is finite if there is a finite simplicial set $K$ and a weak homotopy equivalence $K\rightarrow X$. Finite Kan complexes are precisely (up to equivalence) finite CW complexes.

Question: Now suppose $X$ is a finite Kan complex. It is also a quasicategory. In Higher Topos Theory (1.2.14.2), Lurie takes for granted that $X$ is also finite as a quasicategory. However, this doesn't seem obvious to me. Is there an easy proof?

To see what I mean, take the standard simplicial structure for a circle, with one 0-simplex and one 1-simplex. This describes a finite simplicial set $K$ and a weak homotopy equivalence $f:K\rightarrow S^1$. But $f$ is not a categorical equivalence. To build a finite model for the $\infty$-category $S^1$, we need a second 1-simplex, along with two 2-simplices which declare that the 1-simplices are inverse to each other.

Answer 1

Start from a finite simplicial set $K$ which is homotopicaly equivalent to a Kan complex $X$.

Then by applying a finite number of pushout of outer horn inclusion to $K$, you can build homotopy equivalences $K \hookrightarrow K' \rightarrow X$ such that all the $1$-cells of $K'$ are "invertible" (in the sense that "for all $1$-cell $f$ there exists $2$-cells attesting homotopies $g \circ f => 1$ and $f \circ h => 1$ " see the "edit" below though ). $K'$ is still a finite simplicial set.

I claim that $K' \rightarrow X$ is now an equivalence in the Joyal model structure, which conclude the proof.

Indeed, as all the $1$-cells of $K'$ have homotopy inverses, the homotopy category of $K'$ (in the sense of the left adjoint to the nerve functor) is a groupoid.

So if I take $K' \hookrightarrow Y \rightarrow X$ a factorization as a Joyal trivial cofibration followed by a Joyal fibration, $Y$ is a quasi-category whose homotopy category is equivalent to the homotopy category of $K'$, hence is a groupoid, hence $Y$ is a Kan complex.

And $Y \rightarrow X$ is a homotopy equivalences between Kan complexes, hence it is a Joyal equivalence. So as announced, $K' \rightarrow X$ is a Joyal equivalence.

Edit: small correction and answering your comment. You are indeed right that it is not exactly possible to get what I said. What we need to do precisely is the following:

For each $1$-cell of $K$ you use a pushout by a $\Lambda^0 [2] \hookrightarrow \Delta[2]$ and one by a $\Lambda^2 [2] \hookrightarrow \Delta[2]$ to add a cells $g$ and $h$ with $2$-cells $f \circ g => 1$ and $h \circ f => 1$.

And you stop there, we don't add any new cells (no right inverse for $g$, or left inverse for $h$)

This is enough to ensure that the homotopy category of $K'$ is a groupoids: the original cells of $K$ , like $f$, will be invertible because they have both a left inverse and a right inverse, and the new cells $g$ and $h$ are invertible because they are either right or left inverse to an invertible cell.

As every arrow the homotopy category of $K'$ is a composite of $1$-cell of $K'$ they will all be invertible.