It seems to me that if you are working with structures, i.e. do structural Mathematics you need to understand what they are and they cannot be reduced to their encodings. Hence what is the equality of structures, if not their structural
equality? If I remember correctly, in your talk at Nottingham you discussed a construction by Grothendieck where he used equivalence of structures as if it were equality. This seems to be an omission and you and your students were able to address this, I think
by choosing a canonical representation. However, the funny thing was that you were using a system which doesn’t allow you to express any non-structural properties but because of the way equality is done in Lean you cannot exploit this.
There is something subtle going on which I do not really understand, but it would not surprise me if there are plenty of people on these lists who do. Our problem with formalising the work of Grothendieck was that he assumed that objects which were “canonically” isomorphic were in fact equal. Canonical isomorphism is this weasel word which mathematicians often do not define properly, but in this particular case (we had a proof of P(A) and I could not deduce a proof of P(B) when B was “canonically” isomorphic to A) we solved the problem by noticing that in this particular case “canonically isomorphic” meant “satisfied the same universal property”. We then changed our proof of P(A) to prove instead P(anything satisfying the universal property defining A), and then we were OK. I think it is interesting that at the point in my talk when I explained this, I said “and we couldn’t believe it – our proof barely needed changing” and you laughed and said something like “of course it didn’t!”. We are mathematicians learning how mathematics works 
But we did not go “full univalence”, we did not argue that isomorphic objects were equal, we only needed that “canonically” isomorphic objects were equal. In my experience of mathematics, this is the principle which is used. My fear of univalence is that because it goes a bit further, and that extra step seems to rule out some basic principles used in Lean’s maths library and hence makes a whole bunch of mathematical proofs far more inconvenient to write. I am still learning about theorem provers but am urging my community to start formalising mathematics and this sort of thing is one of many issues which deserves to be better understood – certainly by mathematicians!
I don’t know what Mathematics is actually happening in Maths departments but you seem to agree that it can be done in Type Theory, e.g. in Lean. Indeed, in a way Type Theory is not far away from Mathematical practice (if we ignore the question
of constructiveness for the moment). And it is different from set theory in that it structural by nature. I just find it strange if one cannot go the last step and exploit this fact. It seems somehow this is a blast from the past: because we cannot have univalence
in set theory we don’t need it in type theory either?
I just do not know whether we need it in “Fields Medal mathematics” or whatever you want to call it, because so little “Fields Medal mathematics” is being done in theorem provers. I have this other life when I am going round maths departments arguing that current mathematical practice is extremely unhygenic, producing example after example where I think that pen and paper mathematics has got completely out of control. One thing I have learnt from a couple of years of doing this is that most mathematicians are (a) completely aware of the issues and (b) don’t care. A mathematical historian told me that in fact mathematics has often been like this, basically saying that it is the nature of progress in mathematics research.
Ok, this is a different topic (and I didn’t say anything about constructive Maths in my original posting). I think the sort of Maths you are doing is very much influenced by what you are using it or what it has been used for in the past.
It seems to me that until recently natural science and hardware engineering was the main application of Mathematics and hence influenced what Mathematicians considered as important. The world is changing and computer science and information technology are
becoming an important application of Mathematics. For historical reasons and also for reasons of funding a lot of the Maths for Computer Science is actually done at Computer Science departments. I am just thinking that you, the Mathematicians, maybe miss a
trick here; and so do we, the Computer Scientists because we could profit more from the wisdom of Mathematicians like yourself.
Mathematics is an incredibly broad discipline nowadays, as you say, and serious mathematics is being done in plenty of places other than mathematics departments. The group of people I am trying to “represent”, not necessarily by being one of them, but at least by having what I think is a good understanding of their desires, are those people who do not care about any of these applications, and just want to prove stuff like the p-adic Langlands conjectures, abstract conjectures saying that some class of infinite-dimensional objects coming from analysis are related to actions of an infinite group on some spaces coming from algebra – results which I personally suspect will never have any applications to anything, but which are just intrinsically beautiful and are hence funded because part of the funding system in mathematics firmly believes in blue sky research. The people I’m talking about are beautifully caricatured in “The Ideal Mathematician” https://personalpages.manchester.ac.uk/staff/hung.bui/ideal.pdf by David and Hersh (in fact I slightly struggle to see what is so funny about that article because I so completely understand the point of view of the mathematician). In fact the only difference between some of the mathematicians I know doing “Fields Medal mathematics” and the “ideal mathematician” described in that article is that the areas the “Fields Medal mathematicians” actually work in areas which are taken much more seriously (like the p-adic Langlands philosophy), with very big communities containing powerful people who are making big decisions about where the funding is going within pure mathematics. These people might seem very extreme to many of the people reading these mailing lists – most do not care about computation or constructivism, they spend their lives doing classical reasoning about intrinisically infinite objects, and they do not see the point of these proof assistants at all (and they also do not care about bugs in computer code because the only point of the computer is to check a gazillion examples to convince us that our deep conjectures are true, and we know they’re true anyway). The reason that the computer proof community should be bending over backwards to accommodate these people is that these people are the important ones within pure mathematics, and many of them have very entrenched ideas about what is and isn’t mathematics, and what is and what isn’t important. Thorsten makes some excellent points about all the other places where mathematics is being used but it’s the people at the top of this particular tree who I want. It is these people who should be telling us what kind of type theory should be being used, at least for the system or systems that I believe they will ultimately adopt. But until they notice that the systems exist it is very difficult to get clear answers – or indeed any answers.
As I said to me it seems that too much surface stuff is moved into the core of systems like Lean.
What Lean has going for it is that in practice it is turning out to be very easy to quickly formalise the kind of mathematics which these “top of the tree” pure mathematicians care about. However this might be because of some social phenomena rather than because of its underlying type theory.
Kevin
But we did not go "full univalence", we did not argue that isomorphic objects were equal, we only needed that "canonically" isomorphic objects were equal. In my experience of mathematics, this is the principle which is used. My fear of univalence is that because it goes a bit further, and that extra step seems to rule out some basic principles used in Lean's maths library and hence makes a whole bunch of mathematical proofs far more inconvenient to write. I am still learning about theorem provers but am urging my community to start formalising mathematics and this sort of thing is one of many issues which deserves to be better understood -- certainly by mathematicians!