No soy un experto, pero diría que podría estar realmente interesado en aprender sobre $\infty$ -topos debido a la teoría de tipos de homotopía.
Como he dicho no soy un experto, acabo de empezar a aprender estas cosas así que lo que sigue puede ser incorrecto, pido disculpas de antemano y agradezco a quien me señale algún error.
Por lo que tengo hasta ahora la teoría de tipos de homotopía debería ser el lenguaje interno de un $\infty$ -topos, más o menos como la lógica de orden superior es el lenguaje interno de un topos, o simplemente la teoría de tipos tipados debería ser el lenguaje interno de una categoría cerrada cartesiana, etc....
La teoría de tipos de homotopía es una especie de teoría de tipos dependiente (Martin Löf) con algunos axiomas adicionales, como el axioma de univalencia. Esta clase de teoría de tipos pretende ser una teoría de tipos en la que los tipos deben comportarse como tipos de homotopía de la teoría de homotopía. Por esta razón, este tipo de teoría de tipos puede interpretarse en $\bf SSet$ (la categoría de conjuntos simpliciales) y cualquier otra categoría con suficiente estructura para permitir hacer teoría de homotopía.
De todos modos como he dicho la teoría de tipos de homotopía no es sólo el lenguaje de $\bf SSet$ pero el lenguaje de $\infty$ -topos, por lo que al igual que no estamos limitados a interpretar un lenguaje de primer orden en $\bf Set$ pero podemos usar cualquier topos en su lugar, podemos usar cualquier $\infty$ -topos para interpretar la teoría de tipos de homotopía.
Así pues, por mucho que a uno le interese estudiar la teoría de los topos, ya que son el entorno en el que se puede interpretar HOL, también debería interesarle $\infty$ -topos ya que son las categorías en las que interpretar la teoría de tipos de homotopía.
Si te interesa saber más sobre la teoría de tipos de homotopía puedes empezar a leer el libro o intente echar un vistazo a la página de teoría de tipos de homotopía .
