#HoTT André Joyal correspondance des notions catégoriques et de celles de la théorie homotopique des types

J’ai déjà dit que c’est la grande vertu des travaux d’André Joyal, qui est un des plus grands théoriciens des catégories et des Topoi :

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

éclairer pour les étudiants formés au langage de la théorie des catégories les notations quelquefois abstruses de la théorie homotopique des types ( HoTT = Homotopy type theory)

Ces cours remplissent parfaitement cette tâche :

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

Ainsi la partie 2:

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

Un clan (défini page 5) est une catégorie munie d’une classe F de morphismes ayant certaines propriétés : les flèches de cee classe F sont appelées fibrations.

Une fibration peut être vue (page 8) comme une famille d’objets du clan (de types) .
Une fibration est un morphisme: E ↠ B

La fibre de cette fibration à l’objet x de B ( qui est la flèche 1 → B en bas du diagramme page 8) est l’objet E(x) en haut à gauche du même diagramme (de pullback) ce qui définit une famille de types indexée par x élément variable de B, dite famille interne au clan, qui est donc une collection de telles familles internes, de fibres.

Des exemples de clans sont donnés : la catégorie des complexes de Kan, une catégorie cartésienne (possédant les produits finis).

Un homomorphisme de clans est un foncteur qui préserve l’objet terminal, les fibrations et changements de base de fibrations.

L’extension contextuelle d’un clan E est la catégorie E(A) décrite page 11: c’est la sous-catégorie de la « slice category » E/A (dont les objets sont les flèches ayant pour cible A, un objet de E) : on prend la sous-catégorie en se restreignant aux fibrations .
E(A) a une structure de clan .

Le foncteur E → E(A) défini page 11 est un homomorphisme de clans.
L’objet A est appelé contexte de l’extension, et un objet de E(A) est un type dépendant de contexte A.

Il y a deux types d’égalité en théorie des types : « judgmental » (définitionnelle) et propositionnelle

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

https://ncatlab.org/homotopytypetheory/show/definitional+equality

La première de ces notions est expliquée page 13 sur 37 : c’est une égalité entre types et entre termes d’un même type :

x:A⊢ E(x)=F(x)

x:A ⊢ s(x)=t(x) : E(x)

L’expression x:A est le contexte du jugement .
La deuxième sorte, propositionnelle, d’égalite est introduite plus loin par Joyal:

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

https://arxiv.org/abs/1107.1901

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