Archives quotidiennes :

Cours I de Nicola Gambino sur #HoTT : Type theory

Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types

Pour apprendre la théorie homotopique des types , on a le choix entre étudier les travaux des chercheurs comme André Joyal, Emily Riehl où Michael Shulman, ou bien lire le livre « Homotopy type theory «  sur le blog du même nom :

https://homotopytypetheory.org

A master thesis on homotopy type theory

Il existe de nombreux articles sur les blogs Henosophia:

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/07/hott-the-book-chapitre-1-types-vs-sets/

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/19/hott-the-book-theorie-des-categories-et-des-precategories/

Pour les obtenir taper « #HoTT The book Henosophia »

Mais il y a aussi des cours de Nicola Gambino, sur sa page :

http://www1.maths.leeds.ac.uk/~pmtng/#Slides_of_talks

dont j’ai obtenu l’adresse dans un cours d’André Joyal :

Le cours I est ici :

Il existe une ∞-catégorie de tous les types, qui est peut être un ∞-topos :

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/03/l-∞-categorie-de-tous-les-types/

Page 7 : une théorie des types a pour fonction de dériver des jugements à partir d’autres jugements . Il y a plusieurs sortes de jugements :

A: Type « A est un type »

a:A « …

Voir l’article original 536 mots de plus

Eugenia Cheng : making sense of sets, in theory and life

Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types

Les ensembles ordonnés, qui peuvent être vus comme des catégorie (une flèche entre deux éléments ordonnés selon la relation d’ordre) sont obtenus en ajoutant de la structure à ce qui en est dépourvu : les ensembles..

https://www.wsj.com/articles/making-sense-of-sets-in-theory-and-life-1535643790?redirect=amp#click=https://t.co/1GhKbc2zVQ

Voir l’article original