From Set Theory to Type Theory | The n-Category Café

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 f