[1085] Théorie des types dépendants et axiome d'univalence | Vidéo | Carmin.tv

00:00:00 / 00:00:00

[1085] Théorie des types dépendants et axiome d'univalence

By Thierry Coquand

Appears in collection : Bourbaki - Juin 2014

Cet exposé sera une introduction à la théorie des types dépendants et à l'axiome d'univalence. Cette théorie est une alternative à la théorie des ensembles comme fondement des mathématiques. Guidé par une interprétation d'un type comme un espace topologique « à homotopie près » (type d'homotopie), V. Voevoedsky a introduit une stratiﬁcation des types suivant la complexité de leur égalité, qui fait apparaître la théorie des types comme une généralisation de la théorie des ensembles. Il a aussi formulé l'axiome d'univalence qui est une for me très forte du principe d'extensionalité. On discutera en particulier de quelques conséquences de cet axiome pour la représentation formelle de la notion de catégorie.

Information about the video

Date of recording 21/06/2014
Date of publication 21/06/2014
Institution IHP
Licence CC BY-NC-ND
Language French
Audience Researchers, Graduate Students
Format MP4
Venue IHP - Hermite Amphitheater

Domain(s)

Logic

Bibliography

Séminaire Bourbaki, 66ème année (2013-2014), n°1085, juin 2014 PDF

MSC codes

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

Copyright Carmin.tv 2025

Give feedback