La correspondance entre #CT et #HoTT selon André Joyal

j’ai expliqué ici pourquoi il était nécessaire de réaliser un «  second service » de la partie des articles les plus importants du hashtag #HoTT :

https://scienceinternelle.wordpress.com/2019/02/05/theorie-des-ensembles-set-theory-st-theorie-des-categories-category-theory-ct-theorie-des-types-type-theory-tt-et-theorie-homotopique-des-types-homotopy-type-theory-hott/

Les articles portant sur es travaux d’ André Joyal sont incontestablement les plus importants du hashtag, car ils abordent la question de la relation entre la théorie des catégories (CT ) et la théorie homotopique des types ( HoTT), ce qui est justement l’aspect que j’entends privilégier ici : est ce que HoTT peut être conçue comme une troisième voie intermédiaire entre l’ontologie de la théorie des ensembles ( des universaux abstraits) et l’hénologie de la théorie des catégories  ( théorie des universaux concrets) c’est à dire entre participation à l’être et participation à l’un.  Nous avons la chance d’avoir avec Alain Badiou un philosophe vivant  ( et quel philosophe !) qui se tient strictement  dans la proximité avec la théorie des ensembles , qui est la seule selon lui à représenter l’être, alors que la théorie des catégories et   topoi est plutôt d’ordre logique, portant sur l’apparaitre dans un monde possible; l’être est conçu comme ce qui transcende l’apparaitre dans tous les mondes possibles. Brunschvicg est ici opposé à Badiou comme philosophe de la participation à l’unalors que Badiou est le penseur de la participation à l’être. Mais Brunschvicg n’a pas réalisé de travaux proprement mathématiques d’ailleurs la théorie des catégories n’est née qu’en 1945, après sa mort donc.

L’article à revoir ici est :

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/29/hott-andre-joyal-correspondance-des-notions-categoriques-et-de-celles-de-la-theorie-homotopique-des-types/

qui cite :

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/andre-joyal-hott-and-category-theory/

et le lien de Joyal :

http://logica.dmi.unisa.it/tacl/wp-content/uploads/2014/08/Joyal-TACL2015.pdf

En quatre parties commencé par un survol de TT , la théorie des types ( a sketch of Type theory). La notion de base est le jugement , comme dans la pensée de Brunschvicg

https://fr.m.wikipedia.org/wiki/Léon_Brunschvicg

« Le grand concept brunschvicgien par excellence est celui de jugement dont il expose la théorie dans sa thèse La Modalité du jugement. C’est le jugement qui, dans la réflexion scientifique, constitue le cœur de la philosophie réflexive de Brunschvicg. À partir de ce jugement, qui donne la signification pleine et entière de la conscience intellectuelle, Brunschvicg va pouvoir rendre compte d’une philosophie de l’espri »

C’est un jugement (humain) qui pose l’existence d’un type A (par exemple les entiers naturels N)

⊢ A : Type

ou d’un terme t de A :

⊢ t:A

Ainsi à un ensemble comme N correspond dans TT ou HoTT un type. N peut aussi être vu comme une catégorie , avec une structure d’ordre : une flèche entre un entier n et son successeur n+1t.

La théorie conduit à plusieurs notions de l’égalité :

https://ncatlab.org/nlab/show/equality

Page 7 sur 39 :

Jugement d’égalité de deux termes :

⊢ x ≡ y : A

ou jugement d’égalité de deux types :

⊢ A ≡ B

Un jugement peut être accompagné d’un contexte, dans la théorie des types dépendants d’un paramètre , terme d’un type A :

x:A ⊢ B(x) : Type

Le contexte figure sur la gauche du signe ⊢ de jugement.
Concaténation de contextes :

y: B(x) , x: A ⊢ C(x,y) : Type

Une seconde partie est consacrée aux modèles de la théorie des types, il y en a deux principaux : les groupoides et les ensembles simpliciaux.

https://anthroposophiephilosophieetscience.wordpress.com/2016/09/04/highertopostheory-ensembles-simpliciaux-et-quasi-categories/

https://tractatustoposophicus.wordpress.com/2012/11/18/ensembles-simpliciaux-et-globulaires/

En théorie des modèles (model theory)

https://fr.m.wikipedia.org/wiki/Théorie_des_modèles

une structure mathématique est dite modèle d’une théorie T si les axiomes de T y sont valides. C’est sur la base de cette conception que j’ai caractérisé ce que j’appelle un « mathème » comme « modèle d’une Idée intelligible » , Idée assimilée ici à une théorie axiomatique alors que dans le langage philosophique ce serait plutôt l’inverse : ce sont les Idées qui sont les modèles, et les structure mathématiques ( ce que j’appelle « mathèmes « ) en sont les exemplaires ou copies dans l’esprit humain. J’y reviendrai car il s’agit d’un point crucial : la thèse ( omniprésente dans l’oeuvre de José Dupré) de l’identité de l’Esprit universel ( l’étendue intelligible, lieu des Idées ) et de l’esprit individuel humain ( équation upanishadique atman =brahman) entraîne la relativisation, l’affaiblissement du gouffre entre Idées et idées humaines. Le sens de l’existence humaine est que l’esprit individuel devienne ce qu’il est :l’esprit universel, les idées s’identifiant aux Idées pour n’en être plus les modèles. Tel est le sens du progrès de la conscience dans la philosophie et les mathématiques.

Joyal donne les références des travaux pour ces modèles :Page 16 Hofman et Streicher pour les modèles à base de groupoides, Awodey et Warren Page 17 pour les ensembles simpliciaux

Page 22 il cite en outre différents cadres pour les théories axiomatiques de l’homotopie :

– Verdier et les catégories triangulées

– Quillen et l’algèbre homotopique

– Brown et les catégories de fibrations

– Heller et les théories de l’homotopie

– enfin lasr but not least la théorie des dérivateurs de Grothendieck , qui a été continuée par Maltsinotis

https://ncatlab.org/nlab/show/Georges+Maltsiniotis

Cette partie requiert donc un travail supplémentaire considérable…

Advertisements
This entry was posted in Alain Badiou, category theory, Cochet-Brunschvicg, Ensembles simpliciaux, Higher category theory, Higher topos theory, homotopy type theory, Léon Brunschvicg, Philosophie, Philosophie mathématique, Platon, Science, mathesis, Science-internelle. Bookmark the permalink.