Equivalences of $n$-categories This question is an extension of my previous question last year (see [2020]) in which I asked about the (consensus of a) definition of a weak $n$-category.
Here are some background: while strict $n$-categories are easily defined, they are not sufficient for $n>2$. Therefore weak $n$-categories need to be defined. What a definition of a weak $n$-category should satisfy was proposed in [BD1995]. However, many proposals have since been given (see [Lei2001] or [2020]). And as David White pointed out in [2020], we had not reached to a consensus yet.
This question focuses on a smaller part of the problem.
Question: In order to prove that different models of $n$-categories to be equivalent, there must be a well-defined notion of a $(n+1)$-category to start with. So how is it possible to really prove the equivalence?
I guess this relates to a philosophical problem that in order to justify (anything) one needs to justify the setting in which we justify. Before entering the realm of formalized arguments, we can postulate some desired results (as in [BD1995], or called "specification" in compsci's term), but nothing can stop people from building different settings (or called "implementation" in compsci's term). How could such problem be resolute without brute-force translating results from different foundations?

*

*[2020]: Definition of a $n$-category

*[BD1995]: Higher-dimensional Algebra and Topological Quantum Field Theory-[John C. Baez and James Dolan]-[arXiv:q-alg--9503002]

*[Lei2001]: A Survey of Definitions of n-Category-[Tom Leinster]-[Theory and Applications of Categories, Vol. 10, 2002, No. 1, pp 1-70]

 A: That is indeed a problem, and one could argue that this is part of the reason why these questions are difficult. But I feel that in practice that has never been a strong obstruction. I guess, one way to explain how this apparent paradox disappear is simply to say that nothing forces you to look at $n$-categories as forming an $(n+1)$-categories, especially if you don't know yet what an $(n+1)$-category even is : your $n$-categories (for a concrete definition) are generally organized in a stricter kind of structure and you can show equivalence at some stricter level than as weak $n+1$-categories.
To start with a way too nice example of this, Batanin's definition of $\infty$-category using globular operads and Grothendieck-Maltsiniotis' definition of $\infty$-category using coherator have been shown to be equivalent by Dimitri Ara in his PhD thesis by simply showing they were equivalent as ordinary $1$-category. ( to be precise, part of his results were conditional on a certain faithfulness conjecture that has been proved recently by John Bourke)
Of course, this kind of equivalence is fairly rare and you can't proceed this way very often.
In general, the idea is that one has always been able to prove something so that "for any reasonable definition of $n+1$-category that would produce the equivalence" :
I guess the most typical situation is as follows: each model of $n$-categories we have is organised as an ordinary categories $C$ (whose objects are $n$-categories and morphisms generally corresponds to a notion of strict functors) and a notion of "weak equivalence" of $n$-categories. Generally $C$ is even a Quillen model structure (or rather the full subcategory of fibrant object of such a model category) but that is not really relevant at the level of generality we are talking about. Moreover in each case we know about, the correct notion of "pseudo-functor" can be recovered as a span or cospan of a strict functor and an equivalence'
An equivalence between two such model is then generally presented as a pair of ordinary functors $F:C \to C'$ and $H:C' \to C$ sending weak equivalence to weak equivalence together with zig-zags of natural equivalences connecting $FH$ to $Id_{C'}$ and $HF$ to $Id_C$.
Where by natural equivalence I just mean natural transformation that are objectwise weak equivalence.
Very often all this is done by building Quillen equivalences between Quillen model categories.
Note that what I've described above will only prove that the underlying $(n+1,1)$ categories of $n$-categories are equivalent (i.e. it doesn't take care of comparing higher non-invertible natural transformation). For this you would need in addition that $F$ and $H$ are somehow compatible to certain additional structure on $C$ and $C'$ that encode these. For example certain monoidal closed structure, or other structure that produces the $n$-category of pseudo-functor between two $n$-categories.
But I guess what makes all these comparison results hard to prove is exactly that we have to do this : find some concrete stricter algebraic structure we can talk about and compare and work with constructions that exists at this stricter level...
A: As Marc Hoyois indicates in the comments, historically this was a major obstruction, past tense "was". My feeling is that these days, there is a nice perspective that whatever weak $n$-categories are, they are the objects of some $(\infty,1)$-category $n\mathrm{Cat}$. (Of course, weak $n$-categories are the objects of more than an $(\infty,1)$-category. But the extra $n$ dimensions in $n\mathrm{Cat}$ should be recoverable from looking at exponential objects.) It was a substantial feat to develop a theory of $(\infty,1)$-categories, but it has been more or less done.
Moreover, surely $n\mathrm{Cat}$ will be not just some weird $(\infty,1)$-category, but in fact a presentable $(\infty,1)$-category, and these can be "presented" by model categories. So the question is "just" one of finding the correct Quillen equivalence class of model categories, where "correct" means that it should match your intuition about weak $n$-categories.
Note that I am not saying that there is complete consensus about which presentable $(\infty,1)$-category deserves the name $n\mathrm{Cat}$. I certainly have opinions on the matter (namely: set $0\mathrm{Cat}:= \mathrm{Set}$, and define inductively $n\mathrm{Cat}$ to be the $(\infty,1)$-category of $(\infty,1)$-categories enriched in $(n{-}1)\mathrm{Cat}$), but I don't have the sociological data to conclude that my opinions are shared by the majority, let alone that there exists a consensus.
I should also emphasize that, although I do believe there to be a single correct answer to the question of which presentable $(\infty,1)$-category should be called "$n\mathrm{Cat}$", this answer doesn't satisfy, or at least doesn't obviously satisfy, all natural desiderata. Most notably, it is not very algebraic. I mean, it isn't very non-algebraic — it is about as algebraic as is the notion of "Kan simplicial set" — but it isn't very algebraic either. However, I counter that the search for a highly algebraic theory of $n$-categories is most likely a fool's errand. Any such theory will in particular include a highly algebraic description of homotopy $n$-types. Postnikov and Whitehead provide a "lowly algebraic" description of homotopy $n$-types, and I am pessimistic about there being anything better.
