It is in general not too hard to show that maps between finite $CW$-complexes/finite simplicial sets are homotopy equivalences.

**Question** : Can we do something similar for:

- quasi-categorical equivalences between finite simplicial sets.
- "finitely generated" monoidal quasi-categories. Where by finitely generated I mean in a "polygraphic way" i.e. by a finite sequence of pushout of maps in the image of the free monoid functors.

and eventually more generally for $(\infty,2)$-categories or even $(\infty,n)$-categories.

I'll be more precise:

For homotopy equivalence between finite simplicial sets for example you have an explicit presentation of the $\pi_1$-groupoid given by the $0$,$1$-cell and $2$-cell. If the $\pi_1$ is equivalent to a set then Hurewicz's theorem tells you that you can test if your map is an equivalence on homology, and homology of finite simplicial sets is easy to compute. If the $\pi_1$ are non trivial, it is a bit harder, but you can manage using the homology of the universal cover, or cohomology with value in local coefficient which are also very computable.

To some extent it also works for some infinite simplicial sets if they have explicit enough presentation.

Now I have a precise conjecture that would perfectly answer my question which I would details, but I'm also open to different suggestion.

The case of spaces above can be rephrased as follow:

**Theorem:** The strictification functor from weak $\infty$-groupoids to strict $\infty$-groupoids is conservative. (i.e. detect weak equivalences)

That might require some explanation.

Strict $\infty$-groupoids have been proved by Brown and Higgins to be equivalent to "Crossed complexes". And one can see that Crossed complexes are basically a structure that encodes a $\pi_1$ and what you need to compute a 'twisted' homology.

What I call the strictification functor, is in modern terms the left adjoint to the forgetful functor from strict $\infty$-groupoid to weak $\infty$-groupoid. Such a functor exists because there is a "Folk model structure" on the category of strict $\infty$-groupoids constructed by Brown and Golanski meaning that the homotopy category of this model category is a cocomplete $(\infty,1)$-category and so there is a *unique* left adjoint functor from the $\infty$-category of space to the $\infty$-category of strict $\infty$-groupoid sending terminal object to terminal object.

And it basically corresponds to the construction sending a space to the crossed complex computing its $\pi_1$ and (co)homology (with local coefficient).

So similarly their should be a unique left adjoint functor from the category of $(\infty,n)$-categories to the $\infty$-category of strict $(\infty,n)$-categories (the necessary model structure has been constructed by Ara and Metayer) which send the first $n$ globes to the corresponding globes.

In the case of quasicategories such a functor can for example be constructed by taking the left Kan extension of Street's Orientals, which gives a left adjoint functor from simplicial sets to strict $(\infty,1)$-categories, which I think is a Quillen functor for Joyal model structure and Ara-Metayer's folk structure on strict $(\infty,1)$-category.

**Conjecture**:The strictification functor from weak $(\infty,n)$-categories to strict $(\infty,n)$-categories is conservative.

The two case that are of main interest to me (and that corresponds to the first two points of my original question) is the case of the Kan extension of Street's Orientals from Joyal model structure to strict $(\infty,1)$-categories. And the conservativity of "the functor" from simplicial monoid (with quasi-categorical equivalences) to the category of "one object" $(\infty,2)$-categories (i.e. monoidal $\infty,1$-categories), which essentially corresponds to the second point of my initial question.

comonadic. I suspect it's fairly provable: it would basically be the ultimate version of Mandell's theorem. $\endgroup$ – Charles Rezk Oct 26 '18 at 14:52