Seven Sketches in Compositionality An Invitation to Applied Category Theory (Fong and Spivak)

Category theory is a relatively new branch of mathematics that has transformed much of pure math research. The technical advance is that category theory provides a framework in which to organize formal systems and by which to translate between them, allowing one to transfer knowledge from one field to another. But this same organizational framework also has many compelling examples outside of pure math. In this course, we will give seven sketches on real-world applications of category theory.

What is Order?

Above we informally spoke of two different ordered sets: the order on system connectivity and the order on booleans false ≤ true. Then we related these two ordered sets by means of Alice’s observation Φ. Before continuing, we need to make such ideas more precise. We begin in Section 1.2.1 with a review of sets and relations. In Section 1.2.2 we will give the definition of a preorder— short for preordered set—and a good number of examples.

Review of sets, relations, and functions

We will not give a definition of set here, but informally we will think of a set as a collection of things, known as elements. These things could be all the leaves on a certain tree, or the names of your favorite fruits, or simply some symbols a, b, c. For example, we write A = {h,1} to denote the set, called A, that contains exactly two elements, one called h and one called 1. The set {h, h, 1, h, 1} is exactly the same as A because they both contain the same elements, h and 1, and repeating an element more than once in the notation doesn’t change the set.3

Relationships between different sets for example between the set of trees in your neighborhood and the set of your favorite fruits are captured using subsets and product sets.

Monotone maps

We have said that the categorical perspective emphasizes relationships between things. For example, a preorder is a setting or world in which we have one sort of relationship, ≤, and any two objects may be, or may not be, so-related. Jumping up a level, the categorical perspective emphasizes that preorders themselves each a miniature world composed of many relationships can be related to one another. The most important sort of relationship between preorders is called a monotone map. These are functions that preserve preorder relations in some sense mappings that respect ≤ and are hence considered the right notion of structure-preserving map for preorders.

Meets and Joins

As we have said, a preorder is a set P endowed with an order ≤ relating the elements. With respect to this order, certain elements of P may have distinctive characterizations, either absolutely or in relation to other elements. We have discussed joins before, but we discuss them again now that we have built up some formalism.

Galois Connections

The preservation of meets and joins, and in particular issues concerning generative effects, is tightly related to the theory of Galois connections, which is a special case of a more general theory we will discuss later, namely that of adjunctions. We will use some adjunction terminology when describing Galois connections.

Definition and examples of Galois connections

Galois connections between preorders were first considered by Évariste Galois who didn’t call them by that name in the context of a connection he found between “field extensions” and “automorphism groups.” We will not discuss this further, but the idea is that given two preorders P and Q, a Galois connection is a pair of maps back and forth from P to Q and from Q to P with certain properties, which make it like a relaxed version of isomorphisms. To be a bit more precise, preorder isomorphisms are examples of Galois connections, but Galois connections need not be preorder isomor- phisms.