#HoTT : André Joyal π-tribus et h-tribus; tribus de Martin- Lof et de Voevodsky

Les tribus (« tribes ») se répartissent entre π-tribus et h-tribus ( h pour homotopical):

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

Et se réunifient ensuite comme tribus de Martin-Lof (ML-tribes)(voir tableau page 11 sur 81)

Il existe déjà un article ici :

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/andre-joyal-hott-tribus-et-⊓-tribus/

Autres articles de ce blog consacré aux travaux de Joyal:

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

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

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/20/hott-le-cours-dandre-joyal-en-cinq-parties-sur-les-tribus/

Ainsi que:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/22/hott-andre-joyal-la-notion-de-typos/

Reprenons le travail de Joyal sur les tribus:

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

qui sont des catégories particulières, avec des propriétés supplémentaires (Page 13 sur 81) : ainsi (Page 14) la catégorie Grpd des (petits) groupoides, ou Kan catégorie des complexes de Kan.

Les types sont les objets des catégories appelées tribus, les termes sont catégoriquement les « éléments généralisés » des types, c’est à dire des morphismes dirigés de l’objet terminal vers un type, les tribus peuvent aussi être vues comme des collections de familles puisque les fibrations, définies comme morphismes dans les tribus, sont de telles familles

Page 17 sur 81 : définition des tribus locales C(A) comme sous-catégories de C/A

Les types et termes dépendants sont définis catégoriquement Page 17

La catégorie syntaxique (Page 19) a pour objets les contextes (définis formellement Page 18):

https://ncatlab.org/nlab/show/syntactic+category

Les tribus forment une catégories et aussi une 2-catégorie, en prenant pour 1-fleches les foncteurs définis Page 20 qui sont des homéomorphismes de tribus, et comme 2-fleches les transformations naturelles entre ces foncteurs.
Le foncteur « changement de base » (base change) est adjoint du foncteur « push forward »:

https://ncatlab.org/nlab/show/base+change

La définition du changement de base d’un morphisme p :X → B le long d’un morphisme f : A → B est donnée Page 12 sur 81 : cette construction est possible si et seulement si l’objet (X,p) est quadrable dans la slice category C/B

Le changement de base est un changement de paramètre (reparamétrisation ) voir Page 27 sur 81

Page 31 : une tribu est dite π-fermée, ou encore une π-tribu si toute fibration E → A posséde un produit le long de n’importe quelle fibration f: A → B (les fibrations sont les morphismes de la tribu) et si la flèche de structure (structure map):

Πf(E) → B

est une fibration.

Le produit d’un objet de la slice category C/A le long d’un morphisme f: A → B

est défini page précéente 30 : avec un diagramme on comprend mieux.
C’est, catégoriquement, un espace de sections (Page 29)

Si C est une π-tribu , alors c’est le cas aussi de toute tribu locale C(A) pour tout objet A de C
Puis sont définies les h-tribus ( h pour homotopique) page 35 : ce sont les tribus telles que toute fibration admet une factorisation f=pu avec u anodyne et p fibration. Et, deuxième condition, le changement de base de u anodyne le long d’une fibration est aussi anodyne

Les morphismes anodynes sont définis page 34

https://ncatlab.org/nlab/show/anodyne+morphism

Là encore si C est une h-tribu c’est aussi le cas de toute tribu locale C(A)

Cette note de Joyal est une des plus poussées avec celle sur les « elementary higher toposes » il reste de nombreux point à étudier

Une πh-tribu est une tribu qui est à la fois une π-tribu et une h-tribu : cela donne une ML-tribu Page 51 (tribu de Martin-Lof) si l’on ajoute une condition, l’axiome d’extensionnalité fonctionnelle

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