Pierre Deligne’s talk next week at the Voevodsky Memorial Conference at the Institute for Advanced Study is entitled What do we mean by “equal”.  His abstract suggests that he is broadly sympathetic to univalent foundations:

In the univalent foundation formalism, equality makes sense only between objects of the same type, and is itself a type. We will explain that this is closer to mathematical practice than the Zermelo-Fraenkel notion of equality is.

This could represent a turning point in the (brief) history of univalent foundations, and not primarily because of Deligne’s immense prestige.  Alongside his monumental contributions to mathematics, one of the qualities that made Deligne one of the most admired mathematicians is his unfailing lucidity, as evidenced in his own work as well as in his reformulations of the work of others (here, notoriously, but also here and here, just to mention a few of the examples that directly influenced my own thinking).  If he put his mind to it, Deligne could undoubtedly find a reformulation of univalent foundations that is consistent with (and not merely “closer to”) contemporary norms of mathematical practice.

Deligne’s use of the expression “mathematical practice” is itself remarkable in the light of IAS mathematicians’ historical rejection of sociological tendencies in science studies.  Deligne’s lucidity has been in evidence in his infrequent but eminently quotable interventions that touch on questions of philosophy or sociology of mathematics (see pp. 3-4 of this book, for example).  Unfortunately I will not be able to attend his talk this coming Tuesday but I look forward to watching the video.