Category Theory, Syntactically

November 25, 2016 06:23 UTC (Last updated on September 10, 2024 18:52 UTC)

Tags: programming, math, category theory

(or: How Model Theory Got Scooped by Category Theory)

Overview

This will be a very non-traditional introduction to the ideas behind category theory. It will essentially be a slice through model theory (presented in a more programmer-friendly manner) with an unusual organization. Of course the end result will be ***SPOILER ALERT*** it was category theory all along. A secret decoder ring will be provided at the end. This approach is inspired by the notion of an internal logic/language and by Vaughn Pratt’s paper The Yoneda Lemma Without Category Theory.

I want to be very clear, though. This is not meant to be an analogy or an example or a guide for intuition. This is category theory. It is simply presented in a different manner.

Dan Doel pointed me at some draft lecture notes by Mike Shulman that seem very much in the spirit of this blog post (albeit aimed at an audience familiar with category theory): Categorical Logic from a Categorical Point of View. A theory in my sense corresponds to a category presentation (Definition 1.7.1) as defined by these lecture notes. Its oft-mentioned Appendix A will also look very familiar.

Theories

The first concept we’ll need is that of a theory. If you’ve ever implemented an interpreter for even the simplest language, then most of what follows modulo some terminological differences should be both familiar and very basic. If you are familiar with algebraic semantics, then that is exactly what is happening here only restricting to unary (but multi-sorted) algebraic theories.

For us, a theory, $\mathcal{T}$, is a collection of sorts, a collection of (unary) function symbols¹, and a collection of equations. Each function symbol has an input sort and an output sort which we’ll call the source and target of the function symbol. We’ll write $\mathtt{f}:A\to B$ to say that $\mathtt{f}$ is a function symbol with source $A$ and target $B$. We define $\mathrm{src}(\mathtt{f})\equiv A$ and $\mathrm{tgt}(\mathtt{f})\equiv B$. Sorts and function symbols are just symbols. Something is a sort if it is in the collection of sorts. Nothing else is required. A function symbol is not a function, it’s just a, possibly structured, name. Later, we’ll map those names to functions, but the same name may be mapped to different functions. In programming terms, a theory defines an interface or signature. We’ll write $\mathbf{sort}(\mathcal{T})$ for the collection of sorts of $\mathcal{T}$ and $\mathbf{fun}(\mathcal{T})$ for the collection of function symbols.

A (raw) term in a theory is either a variable labelled by a sort, $$, or it’s a function symbol applied to a term, $$, such that the sort of the term $$ matches the source of $$. The sort or target of a term is the sort of the variable if it’s a variable or the target of the outermost function symbol. The source of a term is the sort of the innermost variable. In fact, all terms are just sequences of function symbol applications to a variable, so there will always be exactly one variable. All this is to say the expressions need to be “well-typed” in the obvious way. Given a theory with two function symbols $$ and $$, $$, $$ , $$, and $$ are all examples of terms. $$ and $$ are not terms because they are not “well-typed”, and $$ by itself is not a term simply because it doesn’t match the syntax. Using Haskell syntax, we can define a data type representing this syntax if we ignore the sorting:

data Term = Var Sort | Apply FunctionSymbol Term

Using GADTs, we could capture the sorting constraints as well:

data Term (s :: Sort) (t :: Sort) where
    Var :: Term t t
    Apply :: FunctionSymbol x t -> Term s x -> Term s t

An important operation on terms is substitution. Given a term $$ with source $$ and a term $$ with target $$ we define the substitution of $$ into $$, written $$, as:

If $$ then $$.

If $$ then $$.

Using the theory from before, we have:

As a shorthand, for arbitrary terms $$ and $$, $$ will mean $$.

Finally, equations². An equation is a pair of terms with equal source and target, for example, $$. The idea is that we want to identify these two terms. To do this we quotient the set of terms by the congruence generated by these pairs, i.e. by the reflexive-, symmetric-, transitive-closure of the relation generated by the equations which further satisfies “if $$ and $$ then $$”. From now on, by “terms” I’ll mean this quotient with “raw terms” referring to the unquotiented version. This means that when we say “$$”, we really mean the two terms are congruent with respect to the congruence generated by the equations. We’ll write $$ for the collection of terms, in this sense, with source $$ and target $$. To make things look a little bit more normal, I’ll write $$ as a synonym for $$ when the intent is that the pair represents a given equation.

Expanding the theory from before, we get the theory of isomorphisms, $$, consisting of two sorts, $$ and $$, two function symbols, $$ and $$, and two equations $$ and $$. The equations lead to equalities like $$. In fact, it doesn’t take much work to show that this theory only has four distinct terms: $$, $$, $$, and $$.

In traditional model theory or universal algebra we tend to focus on multi-ary operations, i.e. function symbols that can take multiple inputs. By restricting ourselves to only unary function symbols, we expose a duality. For every theory $$, we have the opposite theory, $$ defined by using the same sorts and function symbols but swapping the source and target of the function symbols which also requires rewriting the terms in the equations. The rewriting on terms is the obvious thing, e.g. if $$, $$, and $$, then the term in $$, $$ would become the term $$ in $$. From this it should be clear that $$.

Product Theories

Given two theories $$ and $$ we can form a new theory $$ called the product theory of $$ and $$. The sorts of this theory are pairs of sorts from $$ and $$. The collection of function symbols is the disjoint union $$. A disjoint union is like Haskell’s Either type. Here we’ll write $$ and $$ for the left and right injections respectively. $$ takes a function symbol from $$ and a sort from $$ and produces a function symbol of $$ and similarly for $$. If $$ in $$ and $$ is a sort of $$, then $$ and similarly for $$.

The collection of equations for $$ consists of the following:

• for every equation, $$ of $$ and every sort, $$, of $$ we produce an equation $$ by replacing each function symbol $$ in $$ and $$ with $$
• similarly for equations of $$
• for every pair of function symbols $$ from $$ and $$ from $$, we produce the equation $$

The above is probably unreadable. If you work through it, you can show that every term of $$ is equivalent to a pair of terms $$ where $$ is a term in $$ and $$ is a term in $$. Using this equivalence, the first bullet is seen to be saying that if $$ in $$ and $$ is a sort in $$ then $$ in $$. The second is similar. The third then states

To establish the equivalence between terms of $$ and pairs of terms from $$ and $$, we use the third bullet to move all the $$s outward at which point we’ll have a sequence of $$ function symbols followed by a sequence of $$ function symbols each corresponding to term.

The above might seem a bit round about. An alternative approach would be to define the function symbols of $$ to be all pairs of all the terms from $$ and $$. The problem with this approach is that it leads to an explosion in the number of function symbols and equations required. In particular, it easily produces an infinitude of function symbols and equations even when provided with theories that only have a finite number of sorts, function symbols, and equations.

As a concrete and useful example, consider the theory $$ consisting of a single sort, $$, a single function symbol, $$, and no equations. This theory has a term for each natural number, $$, corresponding to $$ applications of $$. Now let’s articulate $$. It has one sort, $$, two function symbols, $$ and $$, and it has one equation, $$. Unsurprisingly, the terms of this theory correspond to pairs of natural numbers. If we had used the alternative definition, we’d have had an infinite number of function symbols and an infinite number of equations.

Nevertheless, for clarity I will typically write a term of a product theory as a pair of terms.

As a relatively easy exercise — easier than the above — you can formulate and define the disjoint sum of two theories $$. The idea is that every term of $$ corresponds to either a term of $$ or a term of $$. Don’t forget to define what happens to the equations.

Related to these, we have the theory $$, which consists of one sort and no function symbols or equations, and $$ which consists of no sorts and thus no possibility for function symbols or equations. $$ has exactly one term while $$ has no terms.

Collages

Sometimes we’d like to talk about function symbols whose source is in one theory and target is in another. As a simple example, that we’ll explore in more depth later, we may want function symbols whose sources are in a product theory. This would let us consider terms with multiple inputs.

The natural way to achieve this is to simply make a new theory that contains sorts from both theories plus the new function symbols. A collage, $$, from a theory $$ to $$, written $$, is a theory whose collection of sorts is the disjoint union of the sorts of $$ and $$. The function symbols of $$ consist for each function symbol $$ in $$, a function symbol $$, and similarly for function symbols from $$. Equations from $$ and $$ are likewise taken and lifted appropriately, i.e. $$ is replaced with $$ or $$ as appropriate. Additional function symbols of the form $$ where $$ is a sort of $$ and $$ is a sort of $$, and potentially additional equations involving these function symbols, may be given. (If no additional function symobls are given, then this is exactly the disjoint sum of $$ and $$.) These additional function symbols and equations are what differentiate two collages that have the same source and target theories. Note, there are no function symbols $$, i.e. where $$ is in $$ and $$ is in $$. That is, there are no function symbols going the “other way”. To avoid clutter, I’ll typically assume that the sorts and function symbols of $$ and $$ are disjoint already, and dispense with the $$s and $$s.

Summarizing, we have $$, $$, and $$ for all $$, $$, $$, and $$. $$ for any $$ and $$ is arbitrarily generated. To distinguish them, I’ll call the function symbols that go from one theory to another bridges. More generally, an arbitrary term that has its source in one theory and target in another will be described as a bridging term.

Here’s a somewhat silly example. Consider $$ that has one bridge $$ with the equations $$ and $$.

More usefully, if a bit degenerately, every theory induces a collage in the following way. Given a theory $$, we can build the collage $$ where the bridges consist of the following. For each sort, $$, of $$, we have the following bridge: $$. Then, for every function symbol, $$ in $$, we have the following equation: $$. We have $$.

You can think of a bridging term in a collage as a sequence of function symbols partitioned into two parts by a bridge. Naturally, we might consider partitioning into more than two parts by having more than one bridge. It’s easy to generalize the definition of collage to combine an arbitrary number of theories, but I’ll take a different, probably worse, route. Given collages $$ and $$, we can make the collage $$ by defining its bridges to be triples of a bridge of $$, $$, a term, $$ of $$, and a bridge of $$, $$ which altogether will be a bridge of $$ going from $$. These triples essentially represent a term like $$. With this intuition we can formulate the equations. For each equation $$ where $$ and $$ are bridges of $$, we have for every bridge $$ of $$ and term $$ of the appropriate sorts $$ and similarly for equations involving the bridges of $$.

This composition is associative… almost. Furthermore, the collages generated by theories, $$, behave like identities to this composition… almost. It turns out these statements are true, but only up to isomorphism of theories. That is, $$ but is not equal.

To talk about isomorphism of theories we need the notion of…

Interpretations

An interpretation of a theory gives meaning to the syntax of a theory. There are two nearly identical notions of interpretation for us: interpretation (into sets) and interpretation into a theory. I’ll define them in parallel. An interpretation (into a theory), $$, is a mapping, written $$ though the superscript will often be omitted, which maps sorts to sets (sorts) and function symbols to functions (terms). The mapping satisfies:

$$ and $$ where $$ and $$ on the right are the domain and codomain operations for an interpretation.

We extend the mapping to a mapping on terms via:

• $$, i.e. the identity function, or, for interpretation into a theory, $$
• $$ or, for interpretation into a theory, $$

and we require that for any equation of the theory, $$, $$. (Technically, this is implicitly required for the extension of the mapping to terms to be well-defined, but it’s clearer to state it explicitly.) I’ll write $$ when $$ is an interpretation of $$ into sets, and $$ when $$ is an interpretation of $$ into $$.

An interpretation of the theory of isomorphisms produces a bijection between two specified sets. Spelling out a simple example where $$ is the set of booleans:

plus the proof $$.

As another simple example, we can interpret the theory of isomorphisms into itself slightly non-trivially.

As an (easy) exercise, you should define $$ and similarly $$. If you defined $$ before, you should define $$ and similarly for $$. As another easy exercise, show that an interpretation of $$ is a bijection. In Haskell, an interpretation of $$ would effectively be foldNat. Something very interesting happens when you consider what an interpretation of the collage generated by a theory, $$, is. Spell it out. In a different vein, you can show that a collage $$ and an interpretation $$ are essentially the same thing in the sense that each gives rise to the other.

Two theories are isomorphic if there exists interpretations $$ and $$ such that $$ and vice versa, and similarly for function symbols. In other words, each is interpretable in the other, and if you go from one interpretation and then back, you end up where you started. Yet another way to say this is that there is a one-to-one correspondence between sorts and terms of each theory, and this correspondence respects substitution.

As a crucially important example, the set of terms, $$, can be extended to an interpretation. In particular, for each sort $$, $$. It’s action on function symbols is the following:

We have, dually, $$ with the following action:

We can abstract from both parameters making $$ which, by an early exercise, can be shown to correspond with the collage $$.

Via an abuse of notation, I’ll identify $$ with $$, though technically we only have an isomorphism between the interpretations, and to talk about isomorphisms between interpretations we need the notion of…

Homomorphisms

The theories we’ve presented are (multi-sorted) universal algebra theories. Universal algebra allows us to specify a general notion of “homomorphism” that generalizes monoid homomorphism or group homomorphism or ring homomorphism or lattice homomorphism.

In universal algebra, the algebraic theory of groups consists of a single sort, a nullary operation, $$, a binary operation, $$, a unary operation, $$, and some equations which are unimportant for us. Operations correspond to our function symbols except that they’re are not restricted to being unary. A particular group is a particular interpretation of the algebraic theory of groups, i.e. it is a set and three functions into the set. A group homomorphism then is a function between those two groups, i.e. between the two interpretations, that preserves the operations. In a traditional presentation this would look like the following:

Say $$ is a group homomorphism from the group $$ to the group $$ and $$ then:

• $$
• $$
• $$

Using something more akin to our notation, it would look like:

The $$ case is the most relevant for us as it is unary. However, for us, a function symbol $$ may have a different source and target and so we made need a different function on each side of the equation. E.g. for $$, $$, and $$ we’d have:

So a homomorphism $$ is a family of functions, one for each sort of $$, that satisfies the above equation for every function symbol of $$. We call the individual functions making up $$ components of $$, and we have $$. The definition for an interpretation into a theory, $$, is identical except the components of $$ are terms of $$ and $$ can be replaced with $$. Two interpretations are isomorphic if we have homomorphism $$ such that each component is a bijection. This is the same as requiring a homomorphism $$ such that for each $$, $$ and $$. A similar statement can be made for interpretations into theories, just replace $$ with $$.

Another way to look at homomorphisms is via collages. A homomorphism $$ gives rise to an interpretation of the collage $$. The interpretation $$ is defined by:

The homomorphism law guarantees that it satisfies the equation on $$. Conversely, given an interpretation of $$, we have the homomorphism, $$. and the equation on $$ is exactly the homomorphism law.

Yoneda

Consider a homomorphism $$. The $$ needs to satisfy for every sort $$ and $$, every function symbol $$, and every term $$:

Looking at this equation, the possibility of viewing it as a recursive “definition” leaps out suggesting that the action of $$ is completely determined by it’s action on the variables. Something like this, for example:

We can easily establish that there’s a one-to-one correspondence between the set of homomorphisms $$ and the elements of the set $$. Given a homomorphism, $$, we get an element of $$ via $$. Inversely, given an element $$, we can define a homomorphism $$ via:

which clearly satisfies the condition on homomorphisms by definition. It’s easy to verify that $$ and immediately true that $$ establishing the bijection.

We can state something stronger. Given any homomorphism $$ and any function symbol $$, we can make a new homomorphism $$ via the following definition:

Verifying that this is a homomorphism is straightforward:

and like any homomorphism of this form, as we’ve just established, it is completely determined by it’s action on variables, namely $$. In particular, if $$, then we have $$. Together these facts establish that we have an interpretation $$ such that $$, the set of homomorphisms, and $$. The work we did before established that we have homomorphisms $$ and $$ that are inverses. This is true for all theories and all interpretations as at no point did we use any particular facts about them. This statement is the (dual form of the) Yoneda lemma. To get the usual form simply replace $$ with $$. A particularly important and useful case (so useful it’s usually used tacitly) occurs when we choose $$, we get $$ or, choosing $$ everywhere, $$ which states that a term from $$ to $$ is equivalent to a homomorphism from $$ to $$.

There is another result, dual in a different way, called the co-Yoneda lemma. It turns out it is a corollary of the fact that for a collage $$, $$ and the dual is just the composition the other way. To get (closer to) the precise result, we need to be able to turn an interpretation into a collage. Given an interpretation, $$, we can define a collage $$ whose bridges from $$ are the elements of $$. Given this, the co-Yoneda lemma is the special case, $$.

Note, that the Yoneda and co-Yoneda lemmas only apply to interpretations into sets as $$ involves the set of homomorphisms.

Representability

The Yoneda lemma suggests that the interpretations $$ and $$ are particularly important and this will be borne out as we continue.

We call an interpretation, $$ representable if $$ for some sort $$. We then say that $$ represents $$. What this states is that every term of sort $$ corresponds to an element in one of the sets that make up $$, and these transform appropriately. There’s clearly a particularly important element, namely the image of $$ which corresponds to an element in $$. This element is called the universal element. The dual concept is, for $$, $$ is co-representable if $$. We will also say $$ represents $$ in this case as it actually does when we view $$ as an interpretation of $$.

As a rather liberating exercise, you should establish the following result called parameterized representability. Assume we have theories $$ and $$, and a family of sorts of $$, $$, and a family of interpretations of $$, $$, both indexed by sorts of $$, such that for each $$, $$ represents $$, i.e. $$. Given all this, then there is a unique interpretation $$ and $$ where $$ and $$ such that $$. To be a bit more clear, the right hand side means $$. Simply by choosing $$ to be a product of multiple theories, we can generalize this result to an arbitrary number of parameters. What makes this result liberating is that we just don’t need to worry about the parameters, they will automatically transform homomorphically. As a technical warning though, since two interpretations may have the same action on sorts but a different action on function symbols, if the family $$ was derived from an interpretation $$, i.e. $$, it may not be the case that $$.

Let’s look at some examples.

As a not-so-special case of representability, we can consider $$ where $$. Saying that $$ represents $$ in this case is saying that bridging terms of sort $$, i.e. sort $$ in $$, in $$, correspond to terms of sort $$ in $$. We’ll call the universal element of this representation the universal bridge (though technically it may be a bridging term, not a bridge). Let’s write $$ for this universal bridge. What representability states in this case is given any bridging term $$ of sort $$, there exists a unique term $$ of sort $$ such that $$. If we have an interpretation $$ such that $$ represents $$ for each sort $$ of $$ we say we have a right representation of $$. Note, that the universal bridges become a family $$. Similarly, if $$ is co-representable for each $$, we say we have a left representation of $$. The co-universal bridge is then a bridging term $$ such that for any bridging term $$ with source $$, there exists a unique term $$ in $$ such that $$. For reference, we’ll call these equations universal properties of the left/right representation. Parameterized representability implies that a left/right representation is essentially unique.

Define $$ via $$ where $$ is some one element set. $$ is the identity function for all function symbols $$. We’ll say a theory $$ has a unit sort or has a terminal sort if there is a sort that we’ll also call $$ that represents $$. Spelling out what that means, we first note that there is nothing notable about the universal element as it’s the only element. However, writing the homomorphism $$ and noting that since there’s only one element of $$ we can, with a slight abuse of notation, also write the term $$ picks out as $$ which gives the equation:

$$ for any function symbol $$ and term, $$, of sort $$, note $$.

This equation states what the isomorphism also fairly directly states: there is exactly one term of sort $$ from any sort $$, namely $$. The dual notion is called a void sort or an initial sort and will usually be notated $$, the analog of $$ will be written as $$. The resulting equation is:

$$ for any function symbol $$, note $$.

For the next example, I’ll leverage collages. Consider the collage $$ whose bridges from $$ consist of pairs of terms $$ and $$. $$ has pairs if $$ has a right representation. We’ll write $$ for the representing interpretation’s action on sorts. We’ll write the universal bridge as $$. The universal property then looks like $$ where $$ is the unique term induced by the bridge $$. The universal property implies the following equations:

One aspect of note is regardless of whether $$ has a right representation, i.e. regardless of whether $$ has pairs, it always has a left representation. The co-universal bridge is $$ and the unique term $$ is $$.

Define an interpretation $$ so that $$ and similarly for function symbols. $$ left represents $$. If the interpretation $$ right represents $$, then we say we have an adjunction between $$ and $$, written $$, and that $$ is left adjoint to $$, and conversely $$ is right adjoint $$.

More generally, whenever we have the situation $$ we say that $$ is left adjoint to $$ or conversely that $$ is right adjoint to $$. We call this arrangement an adjunction and write $$. Note that we will always have this situation if $$ left represents and $$ right represents the same collage. As we noted above, parameterized representability actually determines one adjoint given (its action on sorts and) the other adjoint. With this we can show that adjoints are unique up to isomorphism, that is, given two left adjoints to an interpretation, they must be isomorphic. Similarly for right adjoints. This means that stating something is a left or right adjoint to some other known interpretation essentially completely characterizes it. One issue with adjunctions is that they tend to be wholesale. Let’s say the pair sort $$ existed but no other pair sorts existed, then the (no longer parameterized) representability approach would work just fine, but the adjunction would no longer exist.

Here’s a few of exercises using this. First, a moderately challenging one (until you catch the pattern): spell out the details to the left adjoint to $$. We say a theory has sums and write those sums as $$ if $$. Recast void and unit sorts using adjunctions and/or left/right representations. As a terminological note, we say a theory has finite products if it has unit sorts and pairs. Similarly, a theory has finite sums or has finite coproducts if it has void sorts and sums. An even more challenging exercise is the following: a theory has exponentials if it has pairs and for every sort $$, $$ (note, parameterized representability applies to $$). Spell out the equations characterizing $$.

Finite Product Theories

Finite products start to lift us off the ground. So far the theories we’ve been working with have been extremely basic: a language with only unary functions, all terms being just a sequence of applications of function symbols. It shouldn’t be underestimated though. It’s more than enough to do monoid and group theory. A good amount of graph theory can be done with just this. And obviously we were able to establish several general results assuming only this structure. Nevertheless, while we can talk about specific groups, say, we can’t talk about the theory of groups. Finite products change this.

A theory with finite products allows us to talk about multi-ary function symbols and terms by considering unary function symbols from products. This allows us to do all of universal algebra. For example, the theory of groups, $$, consists of a sort $$ and all it’s products which we’ll abbreviate as $$ with $$ and $$. It has three function symbols $$, $$, and $$ plus the ones that having finite products requires. In fact, instead of just heaping an infinite number of sorts and function symbols into our theory — and we haven’t even gotten to equations — let’s define a compact set of data from which we can generate all this data.

A signature, $$, consists of a collection of sorts, $$, a collection of multi-ary function symbols, and a collection of equations. Equations still remain pairs of terms, but we need to now extend our definition of terms for this context. A term (in a signature) is either a variable, $$ where $$ are sorts and $$, the operators $$ or $$ applied to a term, the unit term written $$ with sort $$, a pair of terms written $$, or the (arity correct) application of a multi-ary function symbol to a series of terms, e.g. $$. As a Haskell data declaration, it might look like:

data SigTerm
    = SigVar [Sort] Int
    | Fst SigTerm
    | Snd SigTerm
    | Unit Sort
    | Pair SigTerm SigTerm
    | SigApply FunctionSymbol [SigTerm]

At this point, sorting (i.e. typing) the terms is no longer trivial, though it is still pretty straightforward. Sorts are either $$, or $$ for sorts $$ and $$, or a sort $$. The source of function symbols or terms are lists of sorts.

• $$
• $$
• $$ where $$
• $$ where $$
• $$ where $$
• $$ where $$ and $$

The point of a signature was to represent a theory so we can compile a term of a signature into a term of a theory with finite products. The theory generated from a signature $$ has the same sorts as $$. The equations will be equations of $$, with the terms compiled as will be described momentarily, plus for every pair of sorts the equations that describe pairs and the equations for $$. Finally, we need to describe how to take a term of the signature and make a function symbol of the theory, but before we do that we need to explain how to convert those sources of the terms which are lists. That’s just a conversion to right nested pairs, $$. The compilation of a term $$, which we’ll write as $$, is defined as follows:

• $$ where $$ means the $$-fold application of $$
• $$
• $$
• $$
• $$
• $$

As you may have noticed, the generated theory will have an infinite number of sorts, an infinite number of function symbols, and an infinite number of equations no matter what the signature is — even an empty one! Having an infinite number of things isn’t a problem as long as we can algorithmically describe them and this is what the signature provides. Of course, if you’re a (typical) mathematician you nominally don’t care about an algorithmic description. Besides being compact, signatures present a nicer term language. The theories are like a core or assembly language. We could define a slightly nicer variation where we keep a context and manage named variables leading to terms-in-context like:

which is

for our current term language for signatures. Of course, compilation will be (slightly) trickier for the nicer language.

The benefit of having compiled the signature to a theory, in addition to being able to reuse the results we’ve established for theories, is we only need to define operations on the theory, which is simpler since we only need to deal with pairs and unary function symbols. One example of this is we’d like to extend our notion of interpretation to one that respects the structure of the signature, and we can do that by defining an interpretation of theories that respects finite products.

A finite product preserving interpretation (into a finite product theory), $$, is an interpretation (into a finite product theory) that additionally satisfies:

where, for $$, $$, $$ is the cartesian product, $$ and $$ are the projections, $$, and $$.

With signatures, we can return to our theory, now signature, of groups. $$ has a single sort $$, three function symbols $$, $$, and $$, with the following equations:

or using the nicer syntax:

An actual group is then just a finite product preserving interpretation of (the theory generated by) this signature. All of universal algebra and much of abstract algebra can be formulated this way.

The Simply Typed Lambda Calculus and Beyond

We can consider additionally assuming that our theory has exponentials. I left articulating exactly what that means as an exercise, but the upshot is we have the following two operations:

For any term $$, we have the term $$. We also have the homomorphism $$. They satisfy:

• $$
• $$ where $$ and $$.

We can view these, together with the the product operations, as combinators, and it turns out we can compile the simply typed lambda calculus into the above theory. This is exactly what the Categorical Abstract Machine did. The “Caml” in “O’Caml” stands for “Categorical Abstract Machine Language”, though O’Caml no longer uses the CAM. Conversely, every term of the theory can be expressed as a simply typed lambda term. This means we can view the simply typed lambda calculus as just a different presentation of the theory.

At this point, this presentation of category theory starts to connect to the mainstream categorical literature on universal algebra, internal languages, sketches, and internal logic. This page gives a synopsis of the relationship between type theory and category theory. For some reason, it is unusual to talk about the internal language of a plain category, but that is exactly what we’ve done here.

I haven’t talked about finite limits or colimits beyond products and coproducts, nor have I talked about even the infinitary versions of products and coproducts, let alone arbitrary limits and colimits. These can be handled the same way as products and coproducts. Formulating a language like signatures or the simply typed lambda calculus is a bit more complicated, but not that hard. I may make a follow-up article covering this among other things. I also have a side project (don’t hold your breath), that implements the internal language of a category with finite limits. The result looks roughly like a simple version of an algebraic specification language like the OBJ family. The RING theory described in the Maude manual gives an idea of what it would look like. In fact, here’s an example of the current actual syntax I’m using.³

theory Categories
    type O
    type A
    given src : A -> O
    given tgt : A -> O

    given id : O -> A
    satisfying o:O | src (id o) = o, tgt (id o) = o

    given c : { f:A, g:A | src f = tgt g } -> A
    satisfying (f, g):{ f:A, g:A | src f = tgt g }
        | tgt (c (f, g)) = tgt f, src (c (f, g)) = src g
    satisfying "left unit" (o, f):{ o:O, f:A | tgt f = o }
        | c (id o, f) = f
    satisfying "right unit" (o, f):{ o:O, f:A | src f = o }
        | c (f, id o) = f
    satisfying "associativity" (f, g, h):{ f:A, g:A, h:A | src f = tgt g, src g = tgt h }
        | c (c (f, g), h) = c (f, c (g, h))
endtheory

It turns out this is a particularly interesting spot in the design space. The fact that the theory of theories with finite limits is itself a theory with finite limits has interesting consequences. It is still relatively weak though. For example, it’s not possible to describe the theory of fields in this language.

There are other directions one could go. For example, the internal logic of monoidal categories is (a fragment of) ordered linear logic. You can cross this bridge either way. You can look at different languages and consider what categorical structure is needed to support the features of the language, or you can add features to the category and see how that impacts the internal language. The relationship is similar to the source language and a core/intermediate language in a compiler, e.g. GHC Haskell and System Fc.

Decoder

If you’ve looked at category theory at all, you can probably make most of the connections without me telling you. The table below outlines the mapping, but there are some subtleties. First, as a somewhat technical detail, my definition of a theory corresponds to a small category, i.e. a category which has a set of objects and a set of arrows. For more programmer types, you should think of “set” as Set in Agda, i.e. similar to the * kind in Haskell. Usually “category” means “locally small category” which may have a proper class of objects and between any two objects a set of arrows (though the union of all those sets may be a proper class). Again, for programmers, the distinction between “class” and “set” is basically the difference between Set and Set1 in Agda.⁴ To make my definition of theory closer to this, all that is necessary is instead of having a set of function symbols, have a family of sets indexed by pairs of objects. Here’s what a partial definition in Agda of the two scenarios would look like:

-- Small category (the definition I used)
record SmallCategory : Set1 where
    field
        objects : Set
        arrows : Set
        src : arrows -> objects
        tgt : arrows -> objects
        ...

-- Locally small category
record LocallySmallCategory : Set2 where
    field
        objects : Set1
        hom : objects -> objects -> Set
        ...

-- Different presentation of a small category
record SmallCategory' : Set1 where
    field
        objects : Set
        hom : objects -> objects -> Set
        ...

The benefit of the notion of locally small category is that Set itself is a locally small category. The distinction I was making between interpretations into theories and interpretations into Set was due to the fact that Set wasn’t a theory. If I used a definition theory corresponding to a locally small category, I could have combined the notions of interpretation by making Set a theory. The notion of a small category, though, is still useful. Also, an interpretation into Set corresponds to the usual notion of a model or semantics, while interpretations into other theories was a less emphasized concept in traditional model theory and universal algebra.

A less technical and more significant difference is that my definition of a theory doesn’t correspond to a category, but rather to a presentation of a category, from which a category can be generated. The analog of arrows in a category is terms, not function symbols. This is a bit more natural route from the model theory/universal algebra/programming side. Similarly, having an explicit collection of equations, rather than just an equivalence relation on terms is part of the presentation of the category but not part of the category itself.

Conclusion

In some ways I’ve stopped just when things were about to get good. I may do a follow-up to elaborate on this good stuff. Some examples are: if I expand the definition so that Set becomes a “theory”, then interpretations also form such a “theory”, and these are often what we’re really interested in. The category of finite-product preserving interpretations of the theory of groups essentially is the category of groups. In fact, universal algebra is, in categorical terms, just the study of categories with finite products and finite-product preserving functors from them, particularly into Set. It’s easy to generalize this in many directions. It’s also easy to make very general definitions, like a general definition of a free algebraic structure. In general, we’re usually more interested in the interpretations of a theory than the theory itself.

While I often do advocate thinking in terms of internal languages of categories, I’m not sure that it is a preferable perspective for the very basics of category theory. Nevertheless, there are a few reasons for why I wrote this. First, this very syntactical approach is, I think, more accessible to someone coming from a programming background. From this view, a category is a very simple programming language. Adding structure to the category corresponds to adding features to this programming language. Interpretations are denotational semantics.

Another aspect about this presentation that is quite different is the use and emphasis on collages. Collages correspond to profunctors, a crucially important and enabling concept that is rarely covered in categorical introductions. The characterization of profunctors as collages in Vaughn Pratt’s paper (not using that name) was one of the things I enjoyed about that paper and part of what prompted me to start writing this. In earlier drafts of this article, I was unable to incorporate collages in a meaningful way as I was trying to start from profunctors. This approach just didn’t add value. Collages just looked like a bizarre curio and weren’t integrated into the narrative at all. For other reasons, though, I ended up revisiting the idea of a heteromorphism. My (fairly superficial) opinion is that once you have the notion of functors and natural transformations, adding the notion of heteromorphisms has a low power-to-weight ratio, though it does make some things a bit nicer. Nevertheless, in thinking of how best to fit them into this context, it was clear that collages provided the perfect mechanism (which isn’t a big surprise), and the result works rather nicely. When I realized a fact that can be cryptically but compactly represented as $$ where $$ is the interval category, i.e. two objects with a single arrow joining them, I realized that this is actually an interesting perspective. Since most of this article was written at that point, I wove collages into the narrative replacing some things. If, though, I had started with this perspective from the beginning I suspect I would have made a significantly different article, though the latter sections would likely be similar.