Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

Collection Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

Organisateur(s) Thierry Coquand
Date(s) 15/06/2022 - 15/06/2022
URL associée https://indico.math.cnrs.fr/event/8052/
00:00:00 / 00:00:00
4 5

Le principe d'univalence: le transfer du raisonnement à traver les equivalence

De Benedikt Ahrens

Le raisonnement à équivalence près est omniprésent en mathématique, et les mathématiciens le font implicitement. Pour les mathématiques sur ordinateurs, ce n'est pas si simple : il faut donner tous les détails éxplicitement. C'est pour cela que Voevodsky a créé les fondements univalents, avec l'objectif de méchaniser le transfer du raisonnement à travers les équivalences. Je présenterai notre travail (avec North, Shulman et Tsementzis) sur le principe d'univalence en fondements univalents, qui met en pratique la vision de Voevodsky.

Informations sur la vidéo

  • Date de captation 15/06/2022
  • Date de publication 20/06/2022
  • Institut IHES
  • Langue Français
  • Audience Chercheurs
  • Format MP4

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow




Inscrivez-vous

  • Mettez des vidéos en favori
  • Ajoutez des vidéos à regarder plus tard &
    conservez votre historique de consultation
  • Commentez avec la communauté
    scientifique
  • Recevez des notifications de mise à jour
    de vos sujets favoris
Donner son avis