Does anyone know a good online resource for type theory? I've heard that in it, there is a "universal object" which "contains" all other "objects." Is this right? Where can I get the good stuff? I know I can google for it; I'm not a moron. I just want your recommendations instead of a list of random pages containing the text "mathematics" "russell" and "type". Thanks a bunch.