#HoTT2 #HigherCategoryTheory théorie des types homotopiques et théorie des ∞-catégories

La thèse de l’homotopie de Grothendieck est, selon cet article :

*****https://arxiv.org/pdf/1807.02177.pdf

 

l’identification des ∞- groupoides et des types homotopiques ( homotopy types) qui forment donc une (∞,1)-catégorie notée ∞Grpd :

 »

∞Grpd is the (∞,1)-category of ∞-groupoids, i.e. of (∞,0)-categories. This is the archetypical (∞,1)-topos, the home of classical homotopy theory. »

https://ncatlab.org/nlab/show/Infinity-Grpd

La théorie de l’homotopie se confond donc avec la théorie des ∞-catégories, ou plus précisément :

https://kerodon.net/tag/0001

théorie des ∞-catégories = homotopie + théorie des catégories 

« The theory of -categories can be viewed as a simultaneous generalization of homotopy theory and category theory. Every Kan complex is an -category, and every category determines an -category (given by the nerve N() »

Certains identifient même, de façon lapidaire, #HoTT ( homotopy type theory) et #HTT ( Higher topos theory):

https://anthroposophiephilosophieetscience.wordpress.com/2019/09/30/hott-httuf-homotopy-type-theory-highertopostheory/

Michael Harris, sur son blog, égalise le langage interne des ∞-topoi et #HoTT :

https://anthroposophiephilosophieetscience.wordpress.com/2020/10/22/language-about-language/

Rejoignant ainsi les thèses de Mike Shulman :

https://arxiv.org/abs/1904.07004

https://golem.ph.utexas.edu/category/2019/04/univalence_in_1toposes.html

 https://anthroposophiephilosophieetscience.wordpress.com/2018/02/05/hott-theorie-homotopique-des-types-∞-cosmoi-et-∞-categories-vers-la-scienceinternelle/

J’avais écrit sur ce blog dès 2018 l’article suivant sur ce thème, contenant tous les liens du hashtag #HoTT (ou pas ) à propos de cette relation évidente de proximité avec les ∞-catégories :

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/05/hott-theorie-homotopique-des-types-∞-cosmoi-et-∞-categories-vers-la-scienceinternelle/

 

This entry was posted in ∞-catégories, ∞-cosmoi, ∞-topoi, Grothendieck, Homotopy, homotopy type theory, HTTUF. Bookmark the permalink.