#HoTT #HTTUF #EHTT #HigherToposTheory ∞- topos

Reprenons donc ces différents hashtag comme je l’ai proposé dans l’article d’hier :

https://anthroposophiephilosophieetscience.wordpress.com/2019/10/01/hott-httuf-ehtt-reprendre-letude-de-highertopostheory/

en commençant par cette page du wiki Nlab consacrée à HoTT et à ses « modèles «  dans les topoi multidimensionnels (« higher toposes »):

https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos

Un (∞,1)-topos est une (∞,1)-catégorie

https://ncatlab.org/nlab/show/(infinity,1)-category

c’est à dire une généralisation de la notion de catégorie :

https://ncatlab.org/nlab/show/infinity-category

où il n’y a pas seulement des flèches entre les objets, mais des morphismes d’ordre supérieur appelés des k-morphismes , k allant de 0 à l’infini ∞ : les 0-morphismes sont les objets, les 1-morphismes relient les objets, les 2-morphismes sont des flèches entre les 1-morphismes et ainsi de suite. Dans une (∞,n)-catégorie, tous les k-morphismes pour k>n sont des équivalences

https://ncatlab.org/nlab/show/equivalence

ou des isomorphismes, c’est à dire des flèches inversibles.

La généralisation de la notion de topos des catégories aux « catégories supérieures »:

https://ncatlab.org/nlab/show/higher+category+theory

et aux  ∞-catégories conduit à l’idée d’∞—topos :

https://ncatlab.org/nlab/show/infinity-topos

Un ∞-topos est un (∞,1)-topos

https://ncatlab.org/nlab/show/%28infinity%2C1%29-topos

de même qu’une ∞-catégorie est une (∞,1)-catégorie.

Des exemples d’∞-topos sont l’∞-catégorie Spaces :

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/11/scienceinternelle-l∞-topos-s-spaces-joue-dans-le-domaine-des-∞-categories-le-role-du-1-topos-set-dans-le-domaine-des-categories/

Ou bien l’(∞,1)-catégorie, notée   ∞Grpd de tous les ∞-groupoides, c’est à dire de toutes les (∞,0)-catégories :

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

« As an (∞,1)-topos ∞Grpd is the terminal (∞,1) (∞,1)-sheaf (∞,1)-topos H there is up to a contractible space of choices a unique geometric morphism (LConst⊣Γ):H→←∞Grpd – the global sectiongeometric morphism. See there for more details. »

La théorie des topoi supérieurs HTT rejoint celle des types homotopiques appelée aussi univalent foundations dans HTTUF, thème  d’une conférence internationale tenue à Leeds en juin dernier :

Home

 

 

 

Allant dans le sens de l’identité : HoTT = Higher topos theory

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

A cette conférence de Leeds de nombreux thèmes ont été abordés :

Prerequisites and abstracts

 

 

notamment le cours donné par Emily Riehl :

 

 

»Emily Riehl “Towards a 2-topos of ∞-categories »

While the category of large categories is not a topos, Lawvere observed that it does possess a topos-like property, with the category of small sets playing a role analogous to the subobject classifier. In this talk, we’ll explain how a 2-topos structure, as axiomatized by Weber and Street, can be deployed to develop the formal category theory of categories. We then describe joint work in progress with Dominic Verity to establish an analogous (∞,2)-topos structure on the 2-category of (∞,1)-categories, that can be deployed to develop a model-independent theory of (∞,1)-categories. »

Je n’ai pas trouvé le texte de cette intervention en juin 2019 d’Emily Riehl, qui travaille avec le savant australien Dominic Verity, mais cet article me semble proche :

la page où l’on trouve tous ses travaux :

http://www.math.jhu.edu/~eriehl/

L’article en question :

http://www.math.jhu.edu/~eriehl/CT2019.pdf

L’exemple paradigmatique de topos (de 1-topos) est Set, nommée Ens dans les articles français, la catégorie des ensembles.

La catégorie CAT de toutes  les (petites) catégories  est un 2-topos.

la 2-catégorie, notée CAT∞ dans le travail de Riehl et Verity, de toutes les ∞-catégories , est un 2-topos.

 

This entry was posted in ∞-catégories, ∞-cosmoi, ∞-topoi, EHTT, Higher category theory, Higher topos theory, homotopy type theory, HTTUF, Science, mathesis, Science-internelle. Bookmark the permalink.