#HoTT analogie des n-types et des n-catégories

Revenant à l’article séminal de Michael Shulman:

http://home.sandiego.edu/~shulman/papers/synhott.pdf

il aborde page 9 section 5 (“identification and equivalences “) la notion de n-types qui forment à partir de n= -2 une échelle infinie semblable à la table périodique des n-catégories :

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

Ainsi , comme pour les n-catégories, les 0-types (n=0) sont les ensembles, il n’y a qu’un seul n-type pour n=-2’qui est le singleton {1}, pour n=-1il y a deux -1-types qui s’identifient aux deux valeurs de vérité 0 et 1, et l’induction (la récurrence ) s’effectue ainsi :

A est un-type si pour tout x:A et y:A le type x=y est un (n-1)-type

L’axiome d’univalence de Voevodsky ” les objets isomorphes sont égaux” encode exactement le principe fondateur du structuralisme.
Ainsi , si l’on dénote par U le type total, appelé “Univers” , le type des ensembles est un sous-type de l’univers qui contient seulement les ensembles , c’est à dire les 0-types. Selon l’axiome d’univalence, deux ensembles isomorphes (en bijection) sont égaux.

Mais dans HoTT le type des ensembles est un 1-type et non lui même un ensemble :c’est une différence importante avec ZFC, c’est à dire ce que Badiou appelle “ontologie” .
L’idée de n-type est en provenance de la théorie de l’homotopie et de sa notion de “homotopy n-type” et dans la théorie des catégories multidimensionnelles cela correspond aux n-groupoides . Voevodsky les appelle ” types of h-level n+2″.

On peut appeler HoTT/UF “théorie synthétique des ∞-groupoides” :ceux ci n’y sont pas définis “schématiquement ” comme ils le sont dans la théorie des ensembles, mais comme dans toute approche axiomatique (et ceci est vrai pour les ensembles dans ZFC) ils n’y sont pas définis explicitement ce qui rend leur théorie bien plus simple dans le cadre de HoTT/UFque dans celui de la théorie des ensembles.
Dans la note 6 Page 5 Mike Shulman identifié HoTT/UF avec ce qui Donne le titre de son article :

” a synthetic theory of higher equalities”

Nous disposons d’une opération sur les types, celle de n-truncation : pour tout type A on définit un n-type [A]n Obtenu à partir de A en “oubliant ” toutes les égalités de niveau supérieur à n

Deux exemples importants sont [A]-1 et [A]0 qui sont la -1-truncation et la 0-truncation de A respectivement le truncation qui ne “se souvient” que de savoir si A est “habité” (contient des éléments) , oubliant toutes les distinction entre ses points , et “se souvient ” seulement de si deux éléments x et y sont ou non égaux , oubliant toute distinction “plus haute ” entre leur distinction de base ( celle de niveau 0).

On voit ici l’analogie avec ce que l’on appelle “foncteurs d’oubli” en théorie des catégories ; ainsi la 0-truncation transforme tout type A en un ensemble, de niveau 0

Advertisements
This entry was posted in ∞-catégories, ∞-cosmoi, ∞-topoi, Grothendieck, Higher category theory, Higher topos theory, homotopy type theory, Logique, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle, Théorie des ensembles (set theory) and tagged . Bookmark the permalink.