Doing laundry now. Need to get food and look at dataset for class project.
Oh my god. Eric Goubault is out of control. If you think you know all there is to know about Curry-Howard, read this. Sheesh. I had a vague dream of locally-partially-ordered topological spaces a couple of years ago (which, I realized only recently, would have a fundamental category instead of a fundamental groupoid, which is kind of interesting) when I was trying to grok differential geometry, but of course the idea has already been pursued by still other people.