Le principe d'univalence: le transfer du raisonnement à traver les equivalence
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.