I know I never post, but this is far too beautiful not to link to, and you should read it.
http://worrydream.com/LadderOfAbstraction/ (I like it totally independent of the random dig at the practicality of type theory, near the end. But I did laugh.)