Generalized elements, functions, and categories
(Part 6 of a series.)
Set theory centers around a twoplace judgment \(x\in X\)—that \(x\) is an element of the set \(X\). Type theories, in contrast, are built on a threeplace judgment \(\Gamma\vdash t:B\)—that under the assumptions \(\Gamma\), \(t\) is a term in the type \(B\). As we will see, the latter notion generalizes the former, and suggests a new way to use sets.
Generalized elements are functions
In a settheoretic model, \([\![\cdot\vdash b:B ]\!]\) is an element of the set \([\![B ]\!]\). \([\![x:A\vdash t:B ]\!]\) is a function \([\![A ]\!]\to[\![B ]\!]\), which sends any element of \([\![A ]\!]\) to an element of \([\![B ]\!]\). Indeed, the substitution
says that an element \(s\) of \([\![A ]\!]\) coupled with such a function \([\![A ]\!]\to[\![B ]\!]\) produces an element \([s/x]t\) of \([\![B ]\!]\).
Notice that, in set theory, \(b\) is an element while \(t\) is a function; in type theory, \(b\) is an element under no assumptions, while \(t\) is an element under the assumption \(x:A\). So we can think of a function \([\![A ]\!]\to[\![B ]\!]\) as an element of \([\![B ]\!]\) pending an element of \([\![A ]\!]\), and an element of \([\![B ]\!]\) as an element of \([\![B ]\!]\) pending nothing (technically, pending an element of \(1\)).
Mathematically, these functions are called generalized elements: for any sets \(X,Y\), an \(X\)element of \(Y\) is a function \(X\to Y\). Then \(t\) is an \([\![A ]\!]\)element of \([\![B ]\!]\), and \(b\) is a \(1\)element of \([\![B ]\!]\). (We also call \(1\)elements global elements, in the sense that they are elements apropos of nothing.)
The idea of generalized elements may seem frivolous, but let us make a few observations. First, they correspond closely to typetheoretic judgments. In a settheoretic model, \([\![\Gamma\vdash t:B ]\!]\) is a \([\![\Gamma]\!]\)element of \([\![B ]\!]\). Conversely, \(f\) is an \(A\)element of \(B\) is basically a threeplace judgment which says that, under the assumptions \(A\), \(t\) is an element of \(B\). Think of it like “\(A\vdash f:B\)” (but mind the scare quotes).
Secondly, generalized elements are defined only in terms of functions between sets, not in terms of sets’ elements themselves. As we will see in the next few posts, this concept is enough to formulate a surprising amount of settheoretic reasoning.
Two simple examples: given a global element of \(A\), and a function \(A\to B\), we can obtain a global element of \(B\) by composing these functions.
A function \(f:A\to B\) is injective if two global elements \(a,a'\) are equal (as functions) whenever their postcompositions by \(f\) are equal (as functions).
Lastly, if we define settheoretic notions purely in terms of functions, as we have started to do above, we can port these definitions directly to more complicated structures by replacing set with foo, and function with functions between foos. (As we will soon see, these ported definitions will even be correct!)
Categories
This is exactly the modus operandi of category theory. A category is essentially a choice of foo and functions between foos satisfying some very basic conditions that allow these kinds of definitions to make sense. The foos of a category are called its objects, and the functions are called its morphisms.
In category theory, we say things like, “In a category where such and such is true, the baz of two objects is defined to be an object which has some morphisms that do such and such.” After a few more definitions, the upshot is that, in any category which has bazzes, every morphism out of a baz happens to be qux.
It can definitely be abstruse at times—some call it abstract nonsense—but the point is that category theory studies patterns which recur in different fields of mathematics, and provides a precise language for relating different sorts of mathematical structures (like type theories and sets!).
On to the definition. A category is a collection of objects \(A,B,C\) and morphisms \(f,g\) which go from an object to an object; \(f:A\to B\) means that \(f\) goes from \(A\) to \(B\). We say \(A\) is the domain of \(f\), and \(B\) the codomain. (It is useful to think of \(f:A\to B\) both as a “function” from \(A\) to \(B\) and as an \(A\)element of \(B\), depending on the situation.)
Furthermore, if we have morphisms \(f:A\to B\) and \(g:B\to C\), we can compose them to obtain a morphism \(gf:A\to C\); composition is associative (\((hg)f=h(gf)\)), and each object \(A\) has an identity morphism \(\textbf{id}_A\) (\(f\textbf{id}_A=f=\textbf{id}_B f\)).
There is a category \(\textbf{Set}\) whose objects are sets, morphisms \(A\to B\) are functions from \(A\) to \(B\), composition is function composition, and identities are identity functions.
\(\textbf{Grp}\) is a category whose objects are groups, and whose morphisms are group homomorphisms; \(\textbf{Top}\) is a category whose objects are topological spaces, and whose morphisms are continuous functions. In both cases, composition and identities are the ordinary notions, and satisfy the necessary equations. There are no nonhomomorphism (resp., discontinuous) functions in \(\textbf{Grp}\) (resp., \(\textbf{Top}\)); we’ll see next time that this is the reason our definitions make sense, so to speak, in these categories.
Here’s one final example of a rather different flavor: recall that a partial order, or poset, is a set equipped with a relation \(\preceq\) which is

reflexive: \(x\preceq x\);

antisymmetric: if \(x\preceq y\) and \(y\preceq x\), then \(x=y\); and

transitive: if \(x\preceq y\) and \(y\preceq z\), then \(x\preceq z\).
Examples include the natural or real numbers with \(\leq\). The subsets of any set form a poset with \(\subseteq\). So does divisibility over the natural numbers: say \(ab\) if \(a\) divides \(b\). Clearly \(aa\); if \(ab\) and \(ba\), then \(a=b\); and if \(ab\) and \(bc\), then \(ac\).
Any poset gives rise to a category whose objects are the elements of the poset, and for any two objects \(A,B\), there is exactly one morphism \(A\to B\) if \(A\preceq B\), and none otherwise.
Why is this a category? By reflexivity, \(A\preceq A\), so there is exactly one morphism \(A\to A\), which must be \(\textbf{id}_A\). Given morphisms \(A\to B\) and \(B\to C\), the transitivity of \(\preceq\) guarantees a unique morphism \(A\to C\), which we define to be the result of composing the morphisms. Associativity and identity follow trivially from the fact that there is at most one morphism between any two objects.