# Why is it worth spending time on type theory?

Looking around there are three candidates for “foundations of mathematics”:

• set theory
• category theory
• type theory

There is a seminal paper relating these three topics:

From Sets to Types to Categories to Sets by Steve Awodey

But at this forum (MSE) and its companion (MO) the tag [type theory] is seriously underrepresented. As of today (2013/11/13) (questions by tag):

MSE

• set theory: 1,866
• category theory: 1,658
• type theory: 39

MO

• set theory: 1,437
• category theory: 1,920
• type theory: 40

Update (2017/05/17):

MSE

• set theory: 4,435
• category theory: 6,137
• type theory: 224

Update (2019/07/15):

MSE

• set theory: 6,267
• category theory: 9,009
• type theory: 371

Update (2020/05/05):

MSE

• set theory: 7,038
• category theory: 10,255
• type theory: 441

What does this mean? Is type theory a hoax? For example, I stumbled over this MSE comment (by a learned member):

[…] a lot of people [in the type theory community] didn’t know
what they really talk about (in comparison to, say, classical
analysis, where the definitions are very concrete and clear). I’m sure
that that’s not 100% true on the actual people, but that impression
did stick with me. […]

I’d like to learn from the MSE- and MO-community (resp. their experts):

Why is it worth spending time on type theory?

Type theory is to set theory what computable functions are to usual functions. It’s a constructive setting for doing mathematics, so it allows to deal carefully with what can or can’t be computed/decided (see intensionality vs. extensionality, or the different notions of reduction and conversion in $\lambda$-calculus). Furthermore, just like category theory, it gives a great insight on how certain mathematical objects are nothing but particular cases of a general construction, in a very abstract and powerful way. Look up the propositions-as-sets and the proofs-as-programs paradigms to see what I mean (but there’s a lot more than that).
First, type theory doesn’t allow abuse of language. For example, in type theory it is usually the case that if $A$ is a set, then a subset of $A$ is not a set. It is a completely different kind of entity: it will probably be a propositional function, i.e. something which maps elements of $A$ to propositions. Another example: if $n$ is a natural number, then $n$ is not an integer (but something like $\mathsf{int}(n)$ will be). Distinctions like these make some mathematicians uncomfortable, but they prove helpful in dealing with certain things which are maybe more interesting to computer scientists (and of course logicians).
Second, there is no “canonical” type theory. Most of the mathematics done in set theory is actually based on $\mathsf{ZFC}$ (or some extension of it). But the fact that there are many different kinds of type theories makes communication between people harder.