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):


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


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

Update (2017/05/17):


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

Update (2019/07/15):


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

Update (2020/05/05):


  • 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?

  • 25
    $\begingroup$ From my, admittedly very shallow, understanding, it is usually argued that type theory is much closer to the way a working mathematician thinks than either set theory or category theory. While set theory is ontologically very simple, you need to jump through all sorts of hoops to construct objects (like the real numbers) that most people actually work with and the constructions tend to leave you with strange artifacts (e.g. the question whether $\emptyset \in \pi$ makes sense to a set theorist but probably no one else). $\endgroup$ Commented Nov 14, 2013 at 21:01
  • 8
    $\begingroup$ A kind of type theory is homotopy type theory, in which you can write proofs on a computer and have them checked. One motivation according to Voevodsky is that homotopy type theory would be better resistant to potential contradictions in mathematics. I know very little about this, and am not convinced myself, but if you are interested in foundations it is at least interesting. He has an expository lecture: video.ias.edu/univalent/voevodsky $\endgroup$
    – user2055
    Commented Nov 14, 2013 at 21:39
  • 6
    $\begingroup$ That bit of homotopy type theory is a little bit oversold and is hardly unique to homotopy type theory (qua type theories). Coq, Agda etc. have been around a long time! $\endgroup$
    – Zhen Lin
    Commented Nov 14, 2013 at 21:51
  • $\begingroup$ @Miha: But what does this imply, concerning the participants of MSE/MO? Aren't they working mathematicians? Shouldn't type theory be much more prominent than set or category theory (with regard to being "much closer to the way a working mathematician thinks")? $\endgroup$ Commented Nov 14, 2013 at 22:00
  • 8
    $\begingroup$ @HansStricker I can't pretend to know why type theory has a smaller presence on MSE/MO. The fact of the matter is that most mathematicians have at least some training in set theory, quite a few know something about category theory, but knowledge of type theory is restricted to a relatively small group (who also tend to call themselves computer scientists instead of mathematicians). Some would call this a historical coincidence. $\endgroup$ Commented Nov 16, 2013 at 19:44

3 Answers 3


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).

Now, as always there are some cons. I'm thinking of two reasons why type theory hasn't had much success among the general mathematicians:

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.

Anyway, there have been many attempts to actually start developing some mathematics in type theories, and some of them have been quite successful: see for instance the work by G. Gonthier with Coq, a proof assistant based on a type theory called the Calculus of Inductive Constructions.

  • 3
    $\begingroup$ I'd argue that type theory allows your second example of abuse of language much more than set theory does. In type theory, subtyping is exactly the notion required. In material set theory, if n is a natural number, n may well also be an integer, but it could be totally the wrong one depending on the encoding. I think the distinction you're pointing out here is between formal and informal maths, which is in principle orthogonal, but culturally/historically related. Your second point is also relevant, in that many type theories do not do this kind of subtyping. $\endgroup$
    – mudri
    Commented Dec 8, 2019 at 1:10
  • $\begingroup$ +1 for a really good introductory answer that I think really hits the nail on the head of the important differences between the 2 approaches to foundations. For the details, a good working knowledge of mathematical logic is needed,though. Basically the advantage of set theory is it's ontological simplicity and the advantage of type theory is that it avoids almost entirely the paradoxes and "counting" problems one runs into in set theory, especially ZFC and it's variants. $\endgroup$ Commented Feb 6, 2021 at 8:11

What exactly is (simple) type theory? After reading some historical accounts on the development of logic, I really wanted to know the answer. However, I kept getting lost in the apparent triviality of the (typed) lambda calculus that I got as answer when I tried to look it up. This sad state of affairs was resolved when I came across "The seven virtues of simple type theory" by William M. Farmer. To my delight and surprise, it turned out that "simple type theory" is an elegant formulation of higher-order logic. There is even a simple and elegant proof system for it, which has the same consistency strength as bounded Zermelo set theory (a predicative system also known as Mac Lane set theory). However, the last claimed virtue in that article is Virtue 7 There are practical extensions of STT that can be effectively implemented. The corresponding section 8 Practicality contained an interesting selection of items from Pandora's box, if I may say so.

Let me add some thoughts in response to Pandora's box and Luca Bressan's comment. There exists many variations of type theory, exactly because it is a very practical logical system. However, this leads to many types of (terminology) confusion. Is "simple type theory" the same thing as "simply typed lambda calculus"? To which extend are polymorphism, subtypes and dependent types important? Are they used by homotopy type theory? What about intuitionistic variants? Is (homotopy) type theory constructive, or at least predicative?

I learned to no longer worry about such questions. I'm just happy that I have now enough prerequisites to better understand some articles about the history of logic. In addition, I can now read article and books which expect a certain familiarity with type theory. This includes material related to Haskell, automatic theorem proving, and of course the HoTT book.

  • 8
    $\begingroup$ Simply typed lambda calculus is just one particular kind of type theory, and also a very weak one, albeit a starting point for many other type theories. $\endgroup$ Commented Nov 16, 2013 at 19:22

Disclaimer: I'm starting to learn type theory, so I'm not an expert.

Personally I've found the following some very good reason to study type theory.

  • For start type theory is a different kind of foundational theory, and sometimes working in different background can be interesting.

  • As Miha Habič pointed out set theory has lot of idiosyncrasy to make all the classical mathematical construction. Type theory is free from those tricky constructions and all the objects are build in a more natural way: although I have to admit that what's natural is a matter of tastes.

  • Type theory has also connections with computability theory: it's a constructive foundational theory and has deep link with computer science, in particular it is a formal system that is also a programming language and so it allows to develop easily proof assistant that can help in verifying correctness of proofs. Doing that in classical set theory can be more difficult, for what I get.

I suppose that there are many other good reason to learn type theory, that I'm not aware for now.

Edit: I've just seen that I haven't addressed the first part, the one about why type theory has so very few question on SE and MO on type theory. Still a guess, but I suppose that is due to two facts:

  • type theory, in it's actual form is quite new, and(apparently that's false, see ZhenLin comment below) before of the Homotopy Type Theory's book I've never heard of a reference which introduce type theory in a intuitive way: I suppose that made type theory really a thing for people interested in computation theory and mathematical logic;
  • almost all the mathematics had be written in terms of sets, this probably contribute in keeping more people interested in set theory rather the type theory.

Anyway I'm thinking that the trend is gonna change especially for the work of homotopy type theorist, I'm really confident that in a not really far future more mathematicians will use type theory as foundational background (many probably already do it without knowing), so it's just a matter of time, or at least that's what I think.

Hope this helps.

  • 6
    $\begingroup$ Type theory is not new! Homotopy type theory is just a version of Martin-Löf type theory, which was created in the 1980s. $\endgroup$
    – Zhen Lin
    Commented Nov 14, 2013 at 22:29
  • 1
    $\begingroup$ @ZhenLin when I say new I was referring to the naive type theory, I don't know of any reference before HoTT book which treat type theory from a non formal point of view. $\endgroup$ Commented Nov 14, 2013 at 23:22
  • 4
    $\begingroup$ That's because extensional type theory is so natural that it needs no introduction! This is what we mean when we say that type theory is closer to how working mathematicians think. $\endgroup$
    – Zhen Lin
    Commented Nov 14, 2013 at 23:27
  • 1
    $\begingroup$ This is an old thread, but if you are looking for a pre-HoTT informal presentation of type theory, then Constable's "Naïve Computational Type Theory" fits the bill: nuprl.org/documents/Constable/NaiveTypeTheoryPreface.html $\endgroup$ Commented Nov 10, 2014 at 4:30
  • 2
    $\begingroup$ @ZhenLin: Can you let me know (or cite references) where this difference is elaborated? $\endgroup$
    – user170039
    Commented Dec 9, 2017 at 4:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .