André Joyal #HoTT : tribus et ⊓-tribus

Les articles d’andré Joyal, comme ceux de Mike Shulman, apportent l’intelligibilité de la théorie des catégories à la théorie homotopique des types, et renforcent le lien entre les deux domaines:

http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf

Le livre de Quillen « Homotopical algebra » qui date de 1967 est la source des découvertes dans le domaine:

https://books.google.fr/books?id=BS4GCAAAQBAJ&pg=PP3&lpg=PP3&dq=quillen+daniel+g.+(1967)+homotopical+algebra&source=bl&ots=UkiF0Sej0Q&sig=g_urpwyS2DLBq9acdA1z820Cx_Y&hl=fr&sa=X&ved=0ahUKEwj23YPAtOrWAhWKvBoKHWxmCYw4ChDoAQgoMAU#v=onepage&q=quillen%20daniel%20g.%20(1967)%20homotopical%20algebra&f=false

https://ncatlab.org/nlab/show/homotopical+algebra

Il existe un lien sur l’algebre homotopique :

http://www.math.cornell.edu/~apatotski/7400-notes-2015.pdf

Un typos est une sorte particulière de tribu (« Tribe ») . La notion de pre -typos est expliquée par Joyal pages 40 et suivantes de ses slides, mais la comprendre nécessite d’avoir assimilé les pages précédentes, qui commencent avec un rappel des idées de Lawvere pages 9 à 21.

Une catégorie cartésienne est une catégorie (Page 8) est une catégorie munie de tous les produits cartésiens (cf page 7) finis (pour un nombre fini d’objets ) et un foncteur est dit cartésien s’il préserve ces produits finis. Une catégorie cartésienne possède notamment un objet terminal (cas particulier de l’existence d’un produit fini ) et pour un objet À un point de A ou élément généralisé ou terme de type A est une flèche de cet objet terminal ⊤ vers A :

a: A : ⊤ → A

Toute théorie algébrique, qui peut être vue comme une catégorie comme l’ont montré les travaux de Lawvere :

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

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

https://ncatlab.org/nlab/show/algebraic+theory

https://ncatlab.org/nlab/show/essentially+algebraic+theory

toute théorie algébrique T donc engendre une catégorie cartésienne C(T), dont les objets sont les produits finis de « sorts », et les flèches sont les opérations de T.

Un modèle de T est un foncteur cartésien de cette catégorie C(T) vers la catégorie Set

Exemple page 10:

La théorie algébrique Mon des monoides

Ensuite sont définie les catégories cartésiennes fermées (existence de l’exponentielle ) dont des exemples sont Set, Cat, Grpd la catégorie des groupoides, et toute catégorie de foncteurs (préfaisceaux) d’une catégorie C vers Set, donc en particulier la catégorie des ensembles simpliciaux

https://ncatlab.org/nlab/show/simplicial+set

Les théories essentiellement algébriques (Page 18):

https://ncatlab.org/nlab/show/essentially+algebraic+theory

Ne sont plus seulement munies de produits finis, mais de toutes les limites finies (un produit est un cas particulier de limite).

Une catégorie est dite localement cartésienne fermée ( Page 20) si la catégorie C/A (Page 14) est cartésienne fermée pour tout objet A de C .
Des exemples de catégories localement cartésiennes fermées sont donnés Page 21, ainsi comme tout topos Set, les préfaisceaux à destination de Set où les topos de Grothendieck; par contre Cat et Grpd ne le sont pas.

Viennent ensuite (pages 22 à 27) les pages sur la notion dûe à Joyal de tribu (tribe) dont les objets sont des types, et Page 28 vient le lien avec les travaux de Lawvere : les tribus sont des théories essentiellement algébriques.

https://ncatlab.org/nlab/show/essentially+algebraic+theory

Ainsi la théorie des catégories peut prendre la forme d’une tribu T(Cat).
Une ⊓-tribu est une tribu ayant des propriétés particulières (pages 29 à 32) . Ce sont des catégories cartésiennes fermées.

Si C est une ⊓- tribu, toute tribu locale C(A) , pour tout objet A de C, est une ⊓-tribu .

Une catégorie localement cartésienne fermée est une ⊓-tribu dans laquelle toute flèche est une fibration (pages 22-23)

La catégorie des groupoides Grpd est une ⊓-tribu si l’on considère que les fibrations sont les iso-fibrations (Page 31)

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