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:
Le livre de Quillen « Homotopical algebra » qui date de 1967 est la source des découvertes dans le domaine:
https://ncatlab.org/nlab/show/homotopical+algebra
Il existe un lien sur l’algebre homotopique :
Click to access 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)
there is nothing to fear but fear itself
Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις 