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]