Well, I’ve always been interested in learning how things really work at the deepest most fundamental level, but somehow, I ended up becoming a number theorist. *shrug* I taught myself some axiomatic set theory when I was younger – but I always thought it was kind of ugly. So imagine my excitement when I came across a new foundational system for mathematics based on type theory. As soon as I saw it, I knew that I needed to learn it! It just looks so sleek and powerful – although I can’t say that I’m in a good position to judge that yet.
My background doesn’t really intersect naturally with any of the ways of thinking about HoTT. I don’t know type theory, except for basic stuff I picked up from programming. I only know a little tiny bit about homotopy theory – just stuff from the first few chapters of Hatcher’s Algebraic Topology. My knowledge of logic is rather minimal, and I don’t really know that much category theory either. I also haven’t used anything like Coq before. So this should be lots of fun!
The reason I wanted to make a blog was just to have a place to write out my ideas, and keep my insights written up somewhere. It might also be nice to have other people giving me feedback and direction, should they stumble across this. And hopefully, it could be helpful for other people interested in learning this stuff but who also don’t really have any background. I don’t want it to be too serious – I feel like I am most creative when things are fun and light-hearted. So yeah, there might be silly things here sometimes :P
There’s another hope I have in learning this, and which actually happens to be how I came across this in the first place. I’ve been interested for some time in the problem of constructing a Friendly Artificial Intelligence – a general artifical intelligence that shares human values, instead of just killing us all or whatever. There’s this organization called MIRI which is doing research on this problem, and their director, Luke Muelhauser, recently interviewed John Baez. And in the comments of the interview on Baez’s blog, Baez started talking about Homotopy Type Theory, and Univalent Foundations! Anyway, may daydream is that maybe thinking about some of the problems (the Tiling Agents problem is the one I have in mind, specifically) from a HoTT perspective might yield some interesting insights. But that is still very far away, and just a dream for now…