#HoTT André Joyal : tribus et clans

La dernière définition est donnée en 2016 dans ce cours en cinq parties:

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

La définition d’un clan est donnée dans le deuxième cours :

https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%202.pdf

pages 4 et 5 sur 37

Les clans sont la notion catégorique qui permettent de formaliser la théorie des types dépendants (« dependent type theory » )

https://ncatlab.org/nlab/show/dependent+type+theory

Un morphisme X → B dans une catégorie E est dit « carrable «  si son produit fibré (pullback) avec n’importe quel morphisme f : A → B

existe .

Le produit fibré (voir Page 4 sur 37) est noté :

A ×B X

Sa projection sur A ( à gauche du diagramme à quatre côtés Page 4) est appelée «  changement de base «  de p le long de f

Une classe F de morphismes dans une catégorie E est fermée par le changement de base si toute flèche dans F est « carrable » et si tout changement de base d’une flèche de F le long d’une flèche dans E appartient à F.

Page 5 : un clan est une catégorie E munie d’un objet terminal

https://en.m.wikipedia.org/wiki/Initial_and_terminal_objects

1 et d’une classe F de morphismes obéissant aux trois conditions suivantes :

– F contient les isomorphismes ( fléches inversibles )
– F est fermée par composition ( c’est à dire que si deux flèches appartiennent à F, leur composée aussi) et changement de base ( voir définition page 4 ou ci dessus)

– l’unique flèche X → 1 appartient à F pour tout objet X de la catégorie E qui est un clan

Les morphismes appartenant à la classe F sont appelés « fibrations »

Les objets d’un clan sont appelés types ; leurs éléments généralisés (fleches dirigées vers eux depuis l’objet terminal) sont appelés termes ou éléments

La définition d’une tribu est donnée dans le troisième cours :

https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%203.pdf

Page 12 sur 32 :

Une tribu est un clan E possédant deux propriétés supplémentaires :

– tout morphisme de E , f : A → B
Admet une factorisation f=pu avec

u : A → X un morphisme anodyne
Et

p : X → B une fibration (c’est à dire un morphisme appartenant à la classe F associée au clan E)

La notion de morphisme anodyne a déjà été vue

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

mais cette notion est expliquée pages 9 et 10 sur 32 : une flèche est dite anodyne si elle a la propriété de « left lifting » ( page 9) par rapport à toute fibration .

Par rapport à la notation dans les liens avant 2015 il y a eu évolution :

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

Ce qui était appelé tribu (tribe) est maintenant appelé clan. Une tribu est un clan ayant des propriétés supplémentaires.

Ce qui était appelé pre-typos est maintenant appelé tribu .

Advertisements
This entry was posted in Philosophie. Bookmark the permalink.