Tag Archives: HoTT

#HoTT Book : introduction

Le livre complet, 500 pages écrites par les experts mondiaux de cette nouvelle discipline, qui permet de fonder les mathématiques à nouveaux frais, et est très proche de la théorie des ∞-catégories et des ∞-Topoi, peut être téléchargé gratuitement ici: … Continue reading

Posted in ∞-catégories, ∞-topoi, homotopy type theory | Tagged , , , , | Leave a comment

#HoTT une théorie “synthétique” des groupoides

Toujours dans l’article : http://home.sandiego.edu/~shulman/papers/synhott.pdf Michael Shulman Page 4 décrit les groupoides comme une généralisation des ensembles comme collections. Il y a deux sortes de collections, dont la seconde est Le collection des manières dont deux objets x et y … Continue reading

Posted in ∞-catégories, ∞-topoi, homotopy type theory, Philosophie | Tagged , , , | Leave a comment

#HoTT : a synthetic approach to higher equalities ( Michael Shulman)

Cet article consacré au rôle de HoTT dans le fondement des mathématiques , est de nature plus philosophique que technique: http://home.sandiego.edu/~shulman/papers/synhott.pdf L’introduction commence avec les différences et les analogies entre ensembles ( sets) et types, qui sont les entités à … Continue reading

Posted in ∞-catégories, homotopy type theory | Tagged , , , ,

#HoTT et théorie des catégories

http://benedikt-ahrens.de/talks/Marseille.pdf Les types, entités qui sont à la base de HoTT et y remplacent les ensembles (ensembles qui sont considérés comme des types particuliers) peuvent être considérés comme des ∞-groupoides. L’axiome des “univalent foundations ” asserte en gros que pour … Continue reading

Posted in ∞-cosmoi, ∞-topoi, homotopy type theory | Tagged , , ,

Les posts de Mike Schulman sur HoTT

https://homotopytypetheory.org/author/mikeshulman/ http://home.sandiego.edu/~shulman/papers/

Posted in homotopy type theory, Philosophie | Tagged ,

HOTT: née de la confrontation de la théorie des types de Martin-Lof et de l’homotopie abstraite

http://home.sandiego.edu/~shulman/papers/synhott.pdf La théorie de Martin-Lof est aussi appelée “dependent type theory” ou “intuitionnistic type theory”: https://ncatlab.org/nlab/show/Martin-Löf+dependent+type+theory https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory http://www.cse.chalmers.se/~bengt/papers/hlcs.pdf Les types sont comme les ensembles des collections , mais qui se comportent différemment des ensembles :ils furent justement utilisés par Russell … Continue reading

Posted in Bertrand Russell, homotopy type theory, Philosophie mathématique, Théorie des ensembles (set theory) | Tagged , , , ,

De Hilbert à Lawvere, Schreiber et HoTT 2 : 1-topos et ∞-topos

Suite du dernier article, commentaires du travail d’Andrei Rodin : http://ffp14.cpt.univ-mrs.fr/DOCUMENTS/SLIDES/RODIN_Andrei.pdf Affirmation page 15 sur 75 : La conception qu’ont Hilbert et Lawvere De l’axiomatisation est significativement différente de ce qu’Andrei Rodin appelle “point de vue épistémologique”, et réaliser cette … Continue reading

Posted in ∞-catégories, ∞-cosmoi, ∞-topoi, homotopy type theory, Ouvert : dualité plan vital-plan spirituel, Science-internelle | Tagged , , , , , ,