Orateur
Prof.
Benedikt AHRENS
(Delft University of Technology)
Description
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 explicitement. C'est pour cela que Voevodsky a créé les fondements univalents, avec l'objectif de mécaniser 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.
