ага, щас, 2014

В 2005-м заметил: "при наличии всей этой красоты и культурного разнообразия в мире какие-то придурки в Москве сидят и бурчат, что русские просто обязаны срочно всем дать по морде."

categories and lambdas

Consider me an idiot, but I do not see anything in type theories that could not be much simpler expressed categorically. Okay, if we have types. If we don't, then it's λ, no? With variations. Also, reading all these κ and ζ theories I get a weird feeling that they are solving problems that were solved 60-70 years ago.

And they constantly use the word "set"! Something like "we introduce a natural numbers object, bla-bla-bla, and we have a set of arrows from such an object to a type..." omfg. That's ridiculous.

Anyway. Sorry.