Satori is pretty weird

I achieved satori, and it's kind of fucked up. Everything is a programming problem. Look at a piece of toast and you'll see an endomorphism on the domain of bread. Look at a chair and you'll see a recursive descent parser. Look at a dog taking a shit and you'll see a novel set of inductive laws for reasoning about infix notation.

I mean, I did swimmingly at the program I was working on, but it would be nice to brush my teeth without having to check my floss for null.

>>26
Most of the core people are not programmers at all. Pretty much everyone doing categorical logic nowadays is involved with HoTT to some extent; the rest of the mathematical establishment simply doesn't show much interest because they never found things on that level of abstraction interesting in their own right to begin with and ZFC is good enough for their purposes that they never need to think about it at all.