#HoTT The Book : chapitre 1 , types vs sets

Le livre, écrit par les meilleurs spécialistes de cette nouvelle discipline, peut être acheté ou téléchargé gratuitement ici:

The HoTT Book

Il vaut mieux apprendre HoTT dans ce livre que lire, comme je le fais, des articles sur Arxiv ou ailleurs, à part les conférences d’André Joyal où Steve Awodey ou Mike Shulman, qui montrent un grand souci pédagogique, les articles que je rebloggue du blog “Homotopy type theory” contiennent souvent les références de tels travaux d’ailleurs.

Cet article vient après celui ci :

https://anthroposophiephilosophieetscience.wordpress.com/2017/08/13/hott-book-introduction/

Donc nous commençons par le paragraphe 1.1 du chapitre 1 “type theory versus Set theory”. Les types peuvent être vus, comme on l’a déjà appris chez Joyal, de deux facons : comme des collections, des sortes d’ensemble dont les éléments sont les “termes” , ou comme des propositions. C’est la thèse des “propositions as types” dans HoTT.Ceci vient du contraste entre les deux théories : celle des ensembles arrive en deux niveaux (layers), la logique mathématique du premier ordre qui gère le calcul des propositions, et l’axiomatique des ensembles proprement dits (par exemple ZFC = Zermelo-Fraenkel + l’axiome du choix). Par contre la théorie des types est son propre système déductif; il n’y a qu’une seule sorte d’entité de base : les types. Les propositions sont un type particulier. HoTT est ainsi un exemple d’un cadre théorique où le dualisme ( entre la forme logique , propre à l’apparaître , des catégories et l’ontologie des ensembles) disparaît , il n’y a que les types, objets de certaines catégories appelées tribus, qui remplacent les catégories, ensembles y compris, comme forme mathématique des Idées. Ce qui est la forme mathématique de l’idéalisme : il n’y a que les Idées. Les types, plutôt que comme des ensembles, sont vus comme des espaces, leurs éléments les termes comme des points dans ces espaces.
C’est le jugement qui est l’élément fondamental de HoTT, comme de la philosophie, nous l’avions déjà noté. Il est noté:

⊢ a:A

Et s’entend en deux sens , selon que le type A est vu plutôt comme un ensemble ou comme une proposition . Dans le premier cas, le jugement plus haut est lu : a est élément, ou en homotopie un point (appartient à ) de A, dans le second cas les termes sont vus comme des preuves de A et le jugement est lu : a est une preuve de A.
Les “Principia mathematica ” (1913)

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/07/les-principia-mathematica-de-bertrand-russell-et-alfred-north-whitehead-1913/

représentent le sommet , inégalé à ce jour, de la logique qui permet de dériver correctement les propositions.

L’égalité est en mathématiques ensemblistes une proposition , en théorie des types, en vertu de la thèse “propositions as types” c’est un type:

Pour deux éléments a, b : A on a le type : a=Ab

Si ce type a au moins un “habitant” , un terme (s’il est habité) a et b sont dits (propositionnellement) égaux.

Là encore l’égalité vient en deux sens : propositionnelle a = b

Ou définitionnelle ( “definitional” ou “judgmental”) , notée:

a ≡ b

Ainsi par exemple si l’on définit f(x) = x2 alors montrer 32 =9 c’est montrer f(3)=9 par définition. La théorie des types vient donc avec deux sortes de jugements:

⊢ a : A
à est un objet de type A
Et

⊢a ≡ b : A

a et b sont des objets définitionellement égaux de type A

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