#HoTT The Book : sets, Logic and types

The HoTT Book

Chapitre 3 page 107

https://www.andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf

http://publish.uwo.ca/~jbell/types.pdf

Nous voyons avec ce triplet « types, sets, categories » que la théorie des types s’insère entre les ensembles et les catégories soit deux systèmes d’Idées qui jouent ici le rôle de représentants du plan ontologique et du plan internel.

La logique rattachée à la théorie des ensembles est « contaminée « par des termes du langage ordinaire, du monde (des logoi) tels que « et », «  ou « , « quel que soit », « il existe », la théorie des types et sa logique se présente donc comme une décontamination et une formalisation. Certains types se comportent comme des ensembles, ce sont les groupoides discrets et les espaces munis de la topologie discrète .

Ceci est formalisé dans la définition 3.1.1.1 page 107

Un type A est un ensemble si pour tout x,y : A et tout :

p,q : x=y

p=q

Les ensembles sont les types pour lesquels il y a un seul chemin d’égalité entre deux éléments.
Selon la thèse « Propositions as types » on a un type IsSet (A)

Qui est défini par :

IsSet (A)≡: Πx,y:AΠp,q:x=y(p=q)

Voir Page 3 de

https://arxiv.org/pdf/1311.4002.pdf

sur les types finis basiques 0 (pas de terme, ou d’habitant ) 1 ( un terme ) et 2 ( deux éléments 0 et 1)

Les (-2)-types sont dits contractibles :

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

Les (-1)-types sont les propositions et les 0-types sont les ensembles, il y a un lien entre les n-types et les n-catégories:

https://anthroposophiephilosophieetscience.wordpress.com/2017/08/06/hott-analogie-des-n-types-et-des-n-categories/

Type theoretic replacement & the n-truncation

Il existe une opération sur les types se comportant de manière similaire à la n-troncature : la modalité

Modules for Modalities

avec une propriété universelle faisant d’un type modal une sous-(∞,1)-catégorie de l’∞-catégorie de tous les types.

Les types 0, 1, et N sont trois exemples de types qui sont aussi des ensembles : ils sont abordés à la page suivante 108.

Le type 2 à deux éléments, appelé type des booléens, est abordé en 1.8 page 35

Advertisements
This entry was posted in homotopy type theory, Philosophie. Bookmark the permalink.