#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 à la base de ZFC et HoTT et sont tous deux des collections d’objets : mais les types viennent accompagnés d’une nouvelle sorte de structures , les ∞-groupoides , qui consistent en les raisons ou manières dont deux éléments sont égaux , HoTT généralise ainsi des théories des ensembles comme la théorie coxnstructiviste de Bishop:

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

http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/palmgren.pdf

mais en autorisant que deux éléments soient “le même ” de plus d’une façon.

Michael Shulman se positionne en faveur de HoTT et de la théorie des ∞-catégories (les deux sont fortement liées ) par rapport à l’ontologie ensembliste privilégiée par Badiou en affirmant Page 2 que “in addition to expanding The mathematical discourse, HoTT-UF represents certain aspects of current mathematical practice more faithfully than Set theory does ”

Autres liens intéressants à ce propos:

https://perso.ens-lyon.fr/jeremy.ledent/internship_report.pdf

http://www.fields.utoronto.ca/sites/default/files/talk-attachments/Gylterud-Friday-1500.pdf

http://www.bristol.ac.uk/media-library/sites/arts/research/homotopy-type/documents/does-hott-provide-a-foundation-for-mathematics.pdf

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