Monthly Archives: October 2017

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

Uncategorized

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

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 :

André 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 :

#HoTT : le cours d’André Joyal en cinq parties sur les tribus

Ainsi la partie 2:

Click to access download

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…

View original post 244 more words

André Joyal #HoTT : tribus et ⊓-tribus

Uncategorized

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

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:

Click to access 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 :

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…

View original post 391 more words

André Joyal : #HoTT and category theory

Uncategorized

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

Voici donc ce lien :

Click to access Joyal-TACL2015.pdf

Récapitulons ce que nous avons déjà appris de Joyal sur les liens entre théorie des catégories et théorie homotopique des types:

Un type est un jugement, possibilité fondamentale de l’humain selon l’idéalisme contemporain qui est la philosophie amenant à la Science Internelle.

Cet acte de jugement vient sous deux formes:

Page 6 : l’assertion que A (par exemple N les entiers naturels) est un type , ce qui est noté:

⊢A : Type

Et Page 7 : l’assertion que x est un élément de type A

⊢x: A

Par exemple le jugement selon lequel 0 est un entier naturel:

⊢0: N

Les tribus (tribes) sont des catégories particulières, ayant certaines propriétés (Page 25)

Les types sont des objets de tribus. Les termes sont des éléments généralisés de ces objets, c’est à dire des flèches venant de l’objet terminal de la catégorie…

View original post 348 more words