Does the concept of a $\infty$-category have a natural definition in the $\infty$-world?

Question

I start with a thesis: the natural notion of equality is additional data (paths/morphisms), not a binary relation (the fact that they exist). So, in particular, with such a constructivization (replacing property $\to$ structure):

• sets $\to$ $\infty$-groupoids
• categories $\to$ $\infty$-categories

At the same time, it is somewhat unsatisfactory that the concepts on the right have much more cumbersome, technical definitions. The natural answer to this would be: definitions are given in terms of sets i.e. from a 1-world perspective and one would expect the concept of a $\infty$-category have a simple and natural definition in the $\infty$-world.

I know this is an important open problem in homotopy type theory, but homotopy type theory is the internal language of a fairly large class of $\infty$-categories (including all $\infty$-topoi anyway). Thus, it is poorer than the $\infty\text{-}\rm{Groupoid}$ internal language (the most expressive $\infty$-topos?).

Questions

1. What is the description of the $\infty\text{-}\rm{Groupoid}$ internal language?
2. Is there a natural definition of the $\infty$-category in this language?

P.S. I don't mean that I see specific reasons why moving from HoTT to the internal language of $\infty\text{-}\rm{Groupoid}$ should help (on the contrary: in 1-world the concept of a category is interpreted in any finitely complete category, no advantages from the expressive means of toposes, much less $\rm{Set}$ is not), but I still can't be sure otherwise.

Answer 1

Homotopy type theory (HoTT) gives a natural internal language for studying $\infty$-groupoids. Riehl and Shulman give an extension of HoTT which gives an analogous internal language for studying $\infty$-categories. Essentially, the Riehl-Shulman framework is able to work because a bit of extra strictness of equality is encoded in the expanded language of their type theory.

However, there is no known way to even define the notion of an $\infty$-category in plain HoTT, without something like the Riehl-Shulman framework extending the basic language. This is closely related to the open problem of defining the type of semi-simplicial types in plain HoTT, and also to the open problem of defining HoTT internally to the language of HoTT.

I think this is a fundamentally important question. As mentioned by the OP, many practitioners of $\infty$-category theory are very attracted to the idea that $\infty$-groupoids, with their weak notion of equality, should be thought of as more fundamental than sets, with their strict notion of equality. But the fact is, we still do not know how to do all the mathematics we want starting purely from the principles of HoTT and weak equality. Both possible resolutions would yield striking pictures:

• If it's possible, then the vision of a fundamentally homotopical world would be vindicated.

• If it's not, then there should be interesting obstructions to study -- we should be able to understand strictness of equality as a "resource" [1] which a logical theory may have to greater or lesser degrees -- on a par with the "resource" of consistency strength. Theories with access to more strictness would be fundamentally "stronger" than theories without such access.

HoTT is still a young field. One day surely we will know which of these possibilities obtain!

[1] I know I got this terminology from someone else, but I can't remember who. Apologies for the lack of attribution!