#HoTT une théorie “synthétique” des groupoides

Toujours dans l’article :

http://home.sandiego.edu/~shulman/papers/synhott.pdf

Michael Shulman Page 4 décrit les groupoides comme une généralisation des ensembles comme collections. Il y a deux sortes de collections, dont la seconde est Le collection des manières dont deux objets x et y sont “égaux ” : c’est un groupoide (ou un ∞-groupoide) considéré comme généralisation d’un ensemble (“Set”).
Au début du paragraphe 3 Page 5 Michael Shulman oppose la “théorie synthétique” des ∞-groupoide sur qu’est HoTT , en gros théorie axiomatique qui précise les règles et axiomes auxquelles doivent obéir ces entités nouvelles à la “théorie analytique” qui définit ce qu’est un ∞-groupoide en termes d’autres entités mathématiques.

Les entités basiques de HoTT se comportent comme des ∞-groupoide sur mais sont appelées “types” . Ces types ont des éléments dont il sont les “collections” . Section 4, les propositions de la logique sont des types à partir desquels on peut former d’autres types ,ainsi si A et B sont des types propositionnels , ceux des propositions P et Q:

A × B est le type (produit cartésien de A et B) de la proposition P ∧ Q , c’est le type formé des paires ordonnées (a,b) avec a :A et b:B.
De même le type :

A → B représente les implications logiques:

P → Q

Dans le dernier paragraphe 7 Page 12 Michael Shulman , comme aussi Page 4, aborde la notion de covariance en physique, omniprésente en Relativité ; on dispose dans HoTT d’un type Mink, qui est un 1-type, dont les points sont les espaces de Minkowski , intervenant en Relativité Restreinte (“special relativity”)
Suivant le point de vue de Jean-Pierre Marquis ( dans “From a geometrical point of view”) la théorie des catégories est conçue comme une généralisation du programme d’Erlangen de Félix Klein qui assigne à la théorie d’Einstein un groupe de symétries, le groupe de Poincaré.

Dans la physique mise en forme par la théorie des Topoi:

https://meditationesdeprimaphilosophia.wordpress.com/quantum-topos/

le principe de covariance d’Einstein devient le principe de tovariance, voir Page 10 de:

https://www.math.tecnico.ulisboa.pt/~xvi-iwgp/talks/KLandsman.pdf

En résumé, l’innovation centrale de HoTT , qui est liée à la théorie des ∞-groupoides, consiste en ce que toute collection porte en elle même la notion d’identification entre les objets, d’identification entre les identifications , et ainsi de suite. Mais pas plus que dans la théorie des ∞-groupoides, les identifications ne peuvent être séparées des objets auxquels elles s’appliquent . HoTT peut donc être appelée ” a synthetic theory of identity types”.

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

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s