Nicola Gambino : cours IV univalent foundations

Venant à la suite de :

https://hottandphilosophy.wordpress.com/2018/09/07/nicola-gambino-cours-iii-homotopical-models-of-type-theory/

Le cours IV est ici :

http://www1.maths.leeds.ac.uk/~pmtng/Slides/HoTT-Lecture4.pdf

La page 5 sur 23 aborde les types dits contractibles , à partir de la formule pour un nouveau type formé à partir du type A :

iscontr (A) = (Σx:A) (Πy: A) IdA( x,y)

Je rappelle le tableau d’équivalence donné dans le cours 1:

http://www1.maths.leeds.ac.uk/~pmtng/Slides/HoTT-Lecture1.pdf

Page 18 sur 39 « Types as propositions »

(Πx:A) B(x) est équivalent à une formule logique universelle : (∀x ∊ A) B(x)

qui se lit : quel que soit x appartenant à A , on a la propriété B(x) satisfaite par x

De même page 18 le type :

(Σx:A)

équivaut à la formule logique existentielle ( ∃ x ∊ A ) B(x)

Il existe x appartenant à A tel que B(x)

La formule du type iscontr(A) se lit donc : il existe un terme x de A tel que pour tout terme y de A on a x=y

Le type A est dit contractile si le type iscontr(A) est habité (contient au moins un point )

La page consacrée aux types contractibles est :

https://ncatlab.org/nlab/show/contractible+type

Ce sont les types de h-level (homotopy level ) 0

Voir le tableau au paragraphe 2 de :

https://ncatlab.org/nlab/show/homotopy+level

On parle aussi en topologie d’espace contractible :

https://en.m.wikipedia.org/wiki/Contractible_space

D’autres types sont définis comme iscontr, le type isequiv par exemple, voir:

https://ncatlab.org/nlab/show/equivalence+in+homotopy+type+theory

(Semantics of isEquiv)

Et

https://math.stackexchange.com/questions/999640/being-contractible-in-homotopy-theory-vs-homotopy-type-theory

On se pose notamment le problème des catégories qui sont contractibles

https://cstheory.stackexchange.com/questions/27262/relating-univalence-for-a-theory-of-cateogries-to-the-skeleton-concept

La notion de fibre homotopique (homotopy fiber ) est définie page 7 sur 23:soit :

f : A → B

La fibre homotopique de f à y : B est le type :

hfiber (f, y ) = (Σx :A) IdB(fx, y )

ce qui permet de définir le type :

isweq (f) = (Πy:B) iscontr (hfiber (f,y))

et l’on dira que f est une équivalence faible si ce type isweq(f) est habité ( a au moins un élément )

Une homotopie entre f et g : A → B est un élément du type:

(Πx :A) Id B(fx,gx)

La partie II contient un retour sur l’axiome d’univalence grâce aux h-levels , qui permet une vision plus générale des mathématiques

Page 9 sur 23:

http://www1.maths.leeds.ac.uk/~pmtng/Slides/HoTT-Lecture4.pdf

Est définie la condition qui permet de parler de type univalent à propos d’ un
type dépendant :

x:A ⊢ B(x) : Type

L’axiome d’univalence se formule alors (Page 10 sur 23):

Le type dépendant :

x:U ⊢ El(x) : Type

Est un type univalent .

Le tableau à la fin de la page 19 sur 23 donne une hiérarchie définie récursivement, avec trois lignes .

Les types. De h-level 0 sont les types contractiles, ceux de h-level 1 sont les h-propositions, ceux de h-level 2 sont les h-ensembles .

Au niveau plus général des mathématiques , cela correspond à la logique pour les h-level 1, à la théorie des ensembles (0-catégories) pour h-level 2 , et pour la case suivante h-level 3 on a comme types les groupoides et comme mathématiques les 1- catégories

On obtient quelque chose de similaire à la table périodique des n-catégories:

https://anthroposophiephilosophieetscience.wordpress.com/2017/01/17/scienceinternelle-7-la-table-periodique-des-n-categories/

et au tableau de la page sur les h-level

https://ncatlab.org/nlab/show/homotopy+level

La hiérarchie des n-types se poursuit à l’infini

https://ncatlab.org/nlab/show/homotopy+n-type

et à l’infini on a les types non tronqués :

https://ncatlab.org/nlab/show/homotopy+type

et au niveau des mathématiques les ∞-groupoides , c’est à dire les (∞,0)-catégories qui forment ∞-Grpd , exemple paradigmatique d’un (∞,1)-topos

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

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

Cette observation de la page

https://ncatlab.org/nlab/show/homotopy+type

est cruciale : un objet d’un (∞,1)-topos T général peut être vu comme un type d’homotopie dans le monde de T.

Ici tout ∞-topos est vu ici, dans la Science internelle, comme un modèle mathématique de l’Idée de monde ( ce qui est appelé dans la littérature exotérique « idée que se propose Dieu en créant le monde)

Cette page Nlab:

https://ncatlab.org/nlab/show/homotopy+type

est très importante et doit être méditée sans relâche.

Advertisements
This entry was posted in ∞-catégories, category theory, Higher category theory, Homotopy, homotopy type theory, Science, mathesis, Science-internelle. Bookmark the permalink.