It was a day. Advisor meeting went okay. I am feeling less doomed for having, for all practical purposes, signed away my soul as a proof irrelevance monkey for some time the moment I started my senior thesis, since it really looks like an interesting corner of the whole logic-type-theory curry-howard tangle. It's not so much an exotic modality, I think, as just a way of sneaking equational theory in the back door. Or maybe it just captures what you really want when you do propositions-as-types, or as in Awodey and Bauer's paper title, propositions-as-[types]. Anyway, I feel pretty confident that it's something. Yeah.
But I have some stuff to chew on for a while, and I think I'll try to submit to TPHOLs for real this time around.
Not a terrible lot else going on. Went to classes, aleksey's talk, got roped into doing puzzlestorm saturday. Asked the algebraic topology prof if all groups arise as fundamental groups of some space (I thought they did) but he didn't know off-hand.