Type theory is well known to programmers (see TypeScript as an example, or the currently very popular TypeSafe.ai. In fact, due to programming, I grew up with type theory as a basis for my understanding of mathematics (and by extension programming), in contrast to most children which are first introduced to set theory in school.
It does however intuitively make sense that these two theories are deeply related: For example, we may have the set \(\{0, 1\}\) and \(\mathbb{N}\), both of which share one common Element \(0\), i.e. \(0 \in \{0\}\) and \(0 \in \mathbb{N}\). In contrast to that, we may have the type \(\texttt{Bool}\) with the terms \(0 : \texttt{Bool}\) and \(1 : \texttt{Bool}\), and the type \(\texttt{Nat}\) with the terms \(0 : \texttt{Nat}\), \(1 : \texttt{Nat}\), \(2 : \texttt{Nat}\), etc. In this case, we have two different terms \(0 : \texttt{Bool}\) and \(0 : \texttt{Nat}\), which are not equal to each other.
There is however a connection which goes very deep, to places most mathematicians do not date to even go (and by extension most programmers will almost certainly never even heat about). We use Topos theory and its Mitchell-Benabou language to connect set theory with type theory.
A topos is a certain kind of category (see this previous post), which has
In particular, all presheaf categories are topoi, and the category of sets is a topos, as it is the presheaf category of the terminal category (which has one object and one morphism).
As we now know that \(\text{Set}\) is a topos, we can use the Mitchell-Benabou language to reason about it. By (Wang and College, n.d., Definition 2.2.2), we have that given a first order theory \(\mathcal{T}\), we associate to each type \(T\) of it, an object \(\llbracket T \rrbracket\) in the the model \(\mathcal{C}\), a category which is a topos. In particular, we associate to types \(T\) the sets \(\llbracket T \rrbracket\) under the assumption that \(\mathcal{C} = \text{Set}\). Similarily, we associate functions to function symbols ad subobjects to relation symbols.
For more information, (Wang and College, n.d.) is a great book about these ideas. Specifically, a first-order theory \(\mathbb{T}\) consists of 1. A collection of types \(A, B, C, \dots\) 2. A collection of function symbols \(f, g, h, \dots\) each of which has a domain and codomain, i.e. \(f : X_1 \times X_n \to Y\) 3. A collection of relation symbols \(R, S, \dots\) of the form \(R \hookrightarrow X_1 \times X_n\).
Then we can assign a model to that theory, by having a category \(\mathcal{C}\) and interpretation for each type, function symbol and relation symbol: 1. \(\llbracket A \rrbracket \in \text{Obj}(\mathcal{C})\) 2. \(\llbracket f \rrbracket \in \text{Hom}_\mathcal{C}(\llbracket X_1 \rrbracket\times\dots \llbracket X_n \rrbracket, \llbracket Y \rrbracket)\) 3. \(\llbracket R \rrbracket \in \text{Mono}_\mathcal{C}(\llbracket R \rrbracket ,\llbracket X_1 \rrbracket\times\dots \llbracket X_n \rrbracket)\)
Now, given a typed first-order theory, we can therefore assign to each type \(T\) a set, if we can model it in the category of sets \(\text{Set}\). In TypeScript, all types simply hold a set of possible values anyway, so it becomes straightforward to make this formal, using the precise language of categorical logic: As we have seen, given a type \(T\), we can assign to it a set \(\llbracket T \rrbracket\) of possible values which inhabit that type.