I should be an awful lot better at explaining hard stuff than I am. This is because before starting mathematics I had one year of journalism and half a year of law in college. Long story, don't ask.(oddly enough, this hasn't helped me much.)But since I am not good at explanations and I would like to improve, I've decided to write down (over)simplified versions of ideas to see if "practice makes perfect". I've decided to start with Vladimir Voevodsky's programme on Univalent Foundations for Mathematics.
There is a couple of reasons for that. First it's one of the more interest-generating new ideas in Category Theory. Some of it it's just because Voevodsky is a Fields medallist and all that. Some is because category theorists have a "chip on their shoulder" as far as other branches of mathematics are concerned. Despite claims in Wikipedia (of all places) that abstract nonsense is a term of endearment, true category theorists know that it's not. It's an insult where more established branches of mathematics want to say that what we do is just dress up old concepts in new language. But thirdly and far more importantly the reason for trying to explain (to myself) what Univalent Foundations is about is that fact that this is the first serious attempt to extract new mathematics from the Curry-Howard isomorphism.
Why does this matter, do you ask? Well, the Curry-Howard iso is something that I've been trying to explain (to myself and others) for the last twenty years and I still haven't got a good way of doing it. So I wanted to use this non-serious medium (I cannot be corrupting the youth or damaging anyone else's reputation in a blog post) to try out a few off the wall ideas.
One of the things that makes explaining other people's work hard is that your own work and ideas keep trying to introduce themselves into the explanation. One has to fight to keep them off. The case of univalent foundations is slightly easier for me, as my own work is very marginally related to them.
No comments:
Post a Comment