The n-Category Café
Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.
The discussion on Tom’s recent post about ETCS, and the subsequent followup blog post of Francois, have convinced me that it’s time to write a new introductory blog post about type theory. So if you’ve been listening to people talk about type theory all this time without ever really understanding it—or if you’re a newcomer and this is the first you’ve heard of type theory—this post is especially for you.
I used to be a big proponent of structural set theory, but although I still like it, over the past few years I’ve been converted to type theory instead. There are lots of reasons for this, the most important of which I won’t say much about until the end. Instead I mostly want to argue for type theory mainly from a purely philosophical point of view, following on from some of the discussion on Tom’s and Francois’ posts.
