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 to 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 internal $\infty\text{-}\rm{Groupoid}$ language (the most expressive $\infty$-topos?).

Questions

1. What is the description of the $\infty\text{-}\rm{Groupoid}$ internal language?
2. Is there a definition of $\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.

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.

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 to 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 internal $\infty\text{-}\rm{Groupoid}$ language (the most expressive $\infty$-topos).

Questions

1. What is the description of the $\infty\text{-}\rm{Groupoid}$ internal language?
2. Is there a definition of $\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.

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 to 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 internal $\infty\text{-}\rm{Groupoid}$ language (the most expressive $\infty$-topos?).

Questions

1. What is the description of the $\infty\text{-}\rm{Groupoid}$ internal language?
2. Is there a definition of $\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.