Le mystère de l’égalité ; la notion de type comme généralisation de la notion d’ensemble

Thierry Coquand

comment représenter la notion d’égalité en théorie des types ;
stratification de Voevodsky des types ;
une définition uniforme de la notion d’équivalence ;
principe d’univalence ;
application à la notion d’égalité des structures mathématiques et comparaison avec la théorie des ensembles.