#HoTT : la théorie homotopique des types pour sortir de l’opposition thématisée par Badiou

Au début de ce blog figure cet article datant de Mars 2015 :

https://anthroposophiephilosophieetscience.wordpress.com/2016/03/15/les-deux-theories-mathematiques-privilegiees-par-badiou-topoi-et-ensembles-correspondant-aux-deux-plans-vital-ontologique-et-spirituel/

et la situation n’a pas changé avec le récent ouvrage « L’immanence des vérités «  où Badiou écrit dans l’Introduction générale page 18:

« Le regretté Jean Toussaint Desanti me signala que, outrepassant la théorie des ensembles, la théorie des catégories proposait une ontologie d’un autre type, fondée non sur la compacité des multiplicités, mais sur le réseau mouvant des relations. J’allai y voir , dur labeur mathématique, pendant des années, et le conclus que l’on pouvait et devait maintenir que le niveau de l’ontologie comme telle est bien la théorie des multiplicités, mais qu’on devait admettre que la théorie des mondes particuliers- la « physique » si l’on veut- était formalisée dans la pensée catégorielle »

En d’autres termes, la théorie des ensembles (les multiplicités pures) continue de formaliser l’ontologie, la pensée de l’être en tant qu’être, tandis que la théorie des catégories et des topoi est associée à la logique de l’apparaitre dans un monde . C’est le tournant de « Logique des mondes :

https://anthroposophiephilosophieetscience.wordpress.com/2016/03/15/theorie-des-ensembles-et-theorie-des-categories-et-des-topoi-selon-alain-badiou/

https://mathesismessianisme.wordpress.com/2013/07/25/badiou-textes-de-logique-des-mondes-et-etre-et-evenement/

https://mathesisuniversalis2.wordpress.com/2015/06/10/objet-relation-et-transcendantal-le-formalisme-de-logiques-des-mondes/

En 2015 existait déjà la théorie homotopique des types ´ qui a émergé vers 2006, des travaux de chercheurs en théorie des catégories :

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/31/hott-levenement-spirituel-de-la-theorie-homotopique-des-types/

Il n’y a qu’une seule mathématique parce qu’il n’y a qu’une seule Raison universelle : la mathématique n’est pas un langage ou une technique, mais une pensée qui permet de « voir les Idées en Dieu » dans l’Etendue intelligible , qui est Une et unique: les Idées intelligibles sont à la fois multiples et Une, grâce à l’Idée de l’Un, qui est la plus haute et les englobe toutes. idée de l’Un qui a pour mathèmes , modèles mathématiques humains, les ∞-cosmoi :

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/05/hott-theorie-homotopique-des-types-∞-cosmoi-et-∞-categories-vers-la-scienceinternelle/

https://anthroposophiephilosophieetscience.wordpress.com/2018/04/22/modeles-des-∞-categories/

https://anthroposophiephilosophieetscience.wordpress.com/2017/01/19/scienceinternelle-8-∞-cosmoi/

Le tournant malebranchiste pris ici implique t’il une rupture avec la doctrine de l’immanence radicale qui est reprise par Badiou, sans le dire clairement, de Brunschvicg ?

Non car il y une relation , une influence des Idées divines sur l’esprit humain dans les mathèmes, modèles mathématiques humains des Idées divines (platoniciennes)

Cela permet aussi de répondre définitivement au vieux problème :les mathématiciens sont ils des découvreurs ou des inventeurs ?

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/06/le-mathematicien-decouvreur-ou-inventeur-idealisme-vs-realisme/

Les deux ! Les mathématiciens inventent, créent les idées humaines qui sont des mathèmes , des modèles mathématiques des Idées divines qu’ils « ont vu » dans l’Etendue intelligible, séjour des Idées
La théorie homotopique des types contient une version des catégories :

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/19/hott-the-book-theorie-des-categories-et-des-precategories/

« Et si Badiou refuse l’Un avec une violence particulière en se revendiquant comme athée, c’est peut être parce qu’il n’admet que l’universalisme abstrait et ontologique des ensembles, c’est à dire d’une catégorie particulière Set qui est un topos, LE paradigme de la notion de topos , où l’Un n’est présent que comme opération, comme « compte-Pour-Un » ensembliste, alors qu’il joue le rôle de morphisme-identité pour toute catégorie . Et la théorie des types ? L’Un s’y trouve aussi (où ne se trouverait il pas?) comme type -identité (identity type )« 

ainsi qu’une version des ensembles, les « h-sets « :

https://hottandphilosophy.wordpress.com/2018/10/24/hott-sets-in-homotopy-type-theory-bas-spitters/

N’en déplaise à Badiou, il y a trois ( et sans doute plus, puisque le progrès de la mathématique n’a aucune limite) manières de « faire un » (Badiou parle de « compte-pour-Un » , de « localisation errante « , « l’Un est une opération , pas une présentation « ) :
– Un ensemble « fait un » de ses éléments

– Un type ( dans #HoTT ) « fait un » de ses termes

– Une catégorie « fait un » de ses objets

Un type peut être vu à la fois comme un ensemble et un espace : deux termes dans un type sont reliés par un « chemin «  , qui est un « habitant «  , un terme d’un nouveau type : le type-identité « de a et b, les deux types de départ :

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

Les termes de ce type identité , noté Id (a=b) doivent être compris comme des « preuves » , des indices ou des témoignages que a = b

Dans un ensemble il n’y a pas de lien entre les éléments, ce que sont les morphismes qui relient les objets dans une catégorie .

Un ensemble est une 0-catégorie, une catégorie est une 1-catégorie :

https://ncatlab.org/nlab/show/n-category

Un ensemble est un 0-type :

https://ncatlab.org/nlab/show/homotopy+0-type

https://ncatlab.org/nlab/show/homotopy+n-type

Advertisements
This entry was posted in Alain Badiou, ∞-catégories, ∞-cosmoi, ∞-topoi, category theory, Higher category theory, Homotopy, homotopy type theory, Léon Brunschvicg, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle, Théorie des ensembles (set theory). Bookmark the permalink.