Théorie de l'homotopie

Je suis de l'avis que les catégories de modèles c'est un outil en théorie de l'homotopie, le vrai objet d'étude c'est les $(\infty,1)$-catégories (pas forcément le modèle à la Joyal-Lurie, mais une notion de ça), et là la réponse à ta question est plus claire.

En effet, il y a deux choses : une intuition/heuristique, et un résultat formel.

L'intuition/heuristique c'est que si tu fais une théorie des types comme HoTT, tu te retrouves avec des types qui ne sont plus forcément discret; par exemple si $x,y : A$ sont deux membres d'un type, $x=_A y$ est un nouveau type, ce n'est pas simplement un énoncé qui est vrai ou faux, c'est tout un nouvel objet; et maintenant si $p,q : x=_A y$ on peut aussi définir le type $p=q$ (j'enlève l'indice pour clarté, mais il devrait être là) qui, à nouveau, n'est pas un énoncé vrai ou faux, mais tout un objet.
En continuant comme ça on se rend compte qu'un type $A$ devient un machin qui ressemble plus vraiment à un ensemble, mais plus à un $\infty$-groupoïde (ou un $\infty$-ensemble :-D ). Il y a des résultats précis à cet effet notamment par Brunerie mais je ne les connais pas. Maintenant, $\infty$-groupoïde, selon l'hypothèse homotopique de Grothendieck, c'est pareil qu'un type d'homotopie (un certain point de vue sur la notion d'espace), ainsi HoTT est plus un théorie des types d'homotopie qu'une théorie à rapprocher de celle des ensembles. Bien sûr, un ensemble définit un type d'homotopie "discret" ("statique" selon la nouvelle terminologie à la Scholze/Clausen mais ne rentrons pas dans ce débat) donc tu as une théorie des ensembles inscrite dans ta théorie des types.

Le résultat formel est relativement récent, il est dû à Shulman (basé sur du travail d'autres gens bien sûr, mais c'est lui qui a mis le coup final), c'est que tout $\infty$-topos est un modèle de HoTT (notamment l'$\infty$-topos des $\infty$-groupoïdes, qui donne une manière de formaliser le paragraphe précédent). Un $\infty$-topos est un type particulier d'$\infty$-catégorie, au même titre qu'un topos est une catégorie avec certaines propriétés; du coup un $\infty$-topos c'est "un endroit où faire de l'homotopie" qui se comporte comme la théorie de l'homotopie originelle (celle des types d'homotopie/$\infty$-groupoïdes)

Chat-Maths: ton dernier paragraphe semble parfaitement justifier le mot "outil" ;-)

Quant au premier, bien sûr on n'a pas utilisé de théorie des $\infty$-catégories jusqu'à récemment, ça ne veut pas dire que ce n'était pas ça, l'objet d'étude fondamental qui était étudié (au travers des catégories de modèles). Qu'en gros, les gens étudiaient l'$\infty$-catégorie sous-jacente, mais n'avaient pas les mots pour le dire, donc étudiaient la catégorie de modèles (et sa catégorie homotopique) comme approximation/présentation.
Mais comme je l'ai dit dans mon premier message, c'est mon avis - pas une vérité universelle ou mathématique.

(PS pour Chat-Maths toujours : si tu veux t'amuser, je te suggère de jeter un oeil au papier, et surtout à la conclusion, où la blague s'arrête, de Krause-Nikolaus "Group theory for homotopy theorists")

(PPS: ce n'est pas tout à fait vrai que les homotopistes ne s'intéressent qu'au présentable, et c'est justement là que le nouveau langage est plus performant - on peut parler de choses petites ou pas bicomplètes, comme les spectres finis, et plein d'autres joyeusetés de ce genre, qui apparaissent vraiment en pratique; alors que dans le cas modèle il faudrait savoir son remplace, avant/après d'avoir fait ce qu'on voulait faire etc. bref c'est embêtant :-D )

Mais ce serait évidemment ridicule de prétendre que les catégories de modèles, "c'est dépassé" ou quelque chose de ce genre.

Chat-Maths : Oui Krause-Nikolaus le message est clair :-D
mais de toute façon, tu as raison de nuancer mes propos, la nuance c'est toujours bien ;-)
Pour ton PS, je connais pas beaucoup Riehl-Verity, j'avais jeté un rapide coup d'oeil il y a quelques mois mais j'ai jamais approfondi. C'est un truc que je voudrais regarder plus en détails un jour (même si au fond de moi l'approche ne me satisfait pas totalement, et je suis beaucoup plus enthousiaste pour l'approche Riehl-Shulman). Si tu as des questions je pourrai quand même essayer mais si c'est technique je ne pourrai certainement rien te dire.