L'axiome d'univalence | Infini 25

L'axiome d'univalence est un axiome moderne introduit par Vladimir Voevodsky. De façon intrigante, il permet d'effectuer des calculs d'homotopie sur des structures pourtant très discrètes.

L'infini et les fondations mathématiques | Playlist Science4All
https://www.youtube.com/playlist?list=PLtzmb84AoqRRgqV5DfE_ykuGQK-vCJ_0t

Homotopy Type Theory on Science4All
http://www.science4all.org/article/type-theory/
http://www.science4all.org/article/homotopy-type-theory/
http://www.science4all.org/article/univalence/

The Homotopy Type Theory Book
https://homotopytypetheory.org/2013/06/20/the-hott-book/

Computer Science ∩ Mathematics (Type Theory) | Computerphile
https://www.youtube.com/watch?v=qT8NyyRgLDQ

Univalent Foundations of Mathematics | Vladimir Voevodsky
https://www.youtube.com/watch?v=9f4pS9s-X2A

Théorie des types dépendants et axiome d'univalence | Thierry Coquand (Séminaire Bourbaki)
https://www.youtube.com/watch?v=T_WcQpj-2to

Univalent foundations subsume classical mathematics | Andrej Bauer
http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

Prossimo episodio

S01E77 - La théorie homotopique des types ??