Univalent foundations and mathematical practice

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.

4 thoughts on “Univalent foundations and mathematical practice

  1. Pingback: Guest post by Kevin Buzzard | Mathematics without Apologies, by Michael Harris

  2. Charles Rezk

    I watched Deligne’s lecture on YouTube. I don’t think there was anything new in it, but I did enjoy his observation that some of the aims of HoTT remind him of the novel 1984, in which the authorities aim to construct a new language in which it becomes impossible to conceive of a heretical thought. (Much as type theory is supposed to prevent you from stating any proposition which is not invariant under isomorphism.)

    Liked by 1 person

    Reply
    1. Yemon Choi

      I haven’t watched the lecture, but I admit that I find it very bizarre for someone to bring up Newspeak in a discussion of HoTT if they are going to be broadly sympathetic to it!

      Like

      Reply

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s