#HoTT The Book : chapitre 1 function types

The HoTT Book

Étant donné les types A et B on peut construire le type:

A → B

des fonctions ( “function”, “map”) de A à B. A la différence de la théorie des ensembles, c’est un concept primitif , et non pas dérivé comme relation fonctionnelle
( une fonction est un sous-ensemble de A × P(B))

Mais l’on a affaire à un type, celui des fonctions de A à B , alors que dans la théorie des catégories c’est un morphisme de A à B,une autre entité que les objets, un 1-morphisme et non un 0-morphisme: ainsi la théorie des catégories garde le souvenir de la dualité principielle, celle de l’Ouvert, tandis que HoTT “écrase ” cette dualité en un monisme, ou une non-dualité, des objets de base, les types.

Univers et familles de types

On introduit des types appelés “Univers” U dont les types sont éléments. Mais l’on rencontre le même paradoxe que Russell en théorie des ensembles si l’on parle d’un type total U dont tous les types sont éléments et qui est donc élément de lui même. Pour pallier à ce paradoxe on introduit une hiérarchie d’univers :

U0 : U1 : U2 etc…

Hiérarchie cumulative c’est à dire que :
Si A : U i alors A : Ui+1

Ceci a l’inconvénient qu’un élément n’a plus un type unique.

Un type est alors un élément , ou “habitant” d’un Univers.

Les types éléments d’un Univers sont dits “petits” (“small types”).

Les fonctions B : A → U

dont le codomaine est un Univers représentent les familles de types variant avec un élément de A

En termes catégoriques (Joyal) cela correspond à une fibration :

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

(Page 16)

C’est une famille d’objets paramétrés par un élément x variable de A et une tribu (sorte de catégorie dont les objets sont les types) est une collection de telles familles.

Une famille est aussi appelée type dépendant (“dependent type”).

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, homotopy type theory. Bookmark the permalink.