Type theory has its origins in an attempt to fix a critical flaw in early versions of set theory, which was identified by the philosopher and logician Bertrand Russell in 1901. Russell noted that some sets contain themselves as a member. For example, consider the set of all things that are not spaceships. This set — the set of non-spaceships — is itself not a spaceship, so it is a member of itself.
Russell defined a new set: the set of all sets that do not contain themselves. He asked whether that set contains itself, and he showed that answering that question produces a paradox: If the set does contain itself, then it doesn’t contain itself (because the only objects in the set are sets that don’t contain themselves). But if it doesn’t contain itself, it does contain itself (because the set contains all the sets that don’t contain themselves).
Russell created type theory as a way out of this paradox. In place of set theory, Russell’s system used more carefully defined objects called types. Russell’s type theory begins with a universe of objects, just like set theory, and those objects can be collected in a “type” called a SET. Within type theory, the type SET is defined so that it is only allowed to collect objects that aren’t collections of other things. If a collection does contain other collections, it is no longer allowed to be a SET, but is instead something that can be thought of as a MEGASET — a new kind of type defined specifically as a collection of objects which themselves are collections of objects.
An important distinction between set theory and type theory lies in the way theorems are treated. In set theory, a theorem is not itself a set — it’s a statement about sets. By contrast, in some versions of type theory, theorems and SETS are on equal footing. They are “types” — a new kind of mathematical object. A theorem is the type whose elements are all the different ways the theorem can be proved. So, for example, there is a single type that collects all the proofs to the Pythagorean theorem.
The article goes on to discuss Vladimir Voevodsky reasonings for the adaptation of a new type theory informed by homotopy theory as a replacement for set theory in mathematics. This would allow computers to check all mathematical proofs—which apparently we can’t currently do with set theory.