# An Axiomatic Theory of Structure

# Categories, Functors, Natural Transformations

(not in final form)

This is the center piece of my [Short of Introduction to Monads](https://hackmd.io/@alexhkurz/H1OxumxRP). While we have already seen many examples of categories, functors and natural transformations (without calling them that), we will now meet the mathematical definitions. This will allow us, in the next lecture, to define a monad $(M,\eta,\mu)$ as a functor $M$ together with two natural transformations $\eta$ and $\mu$ satisfying the (suitably adapted) monoid laws.

I started the lecture with the following tower of abstractions:

- Numbers are example of monoids.
- Monoids are examples of algebras.
- Algebras organise themselves as categories.

In the last lecture we have seen our first definition of algebraic structures as mathematical objects specified by operations and equations.

Now we are going to present an **axiomatic theory of structure**.

In the lecture we went through the Axioms and then tried to characterize the polymorphic functions/natural transformations of the types indicated in [polymorphic.hs](https://repl.it/@alexhkurz/polymorphic#main.hs) do exist. We skipped the other material in this write-up.

Programs: [`polymorphic`](https://repl.it/@alexhkurz/polymorphic#main.hs).

## Examples

In terms of the hierarchy of abstractions above, the important example is that, given a signature $\Sigma$, the collection of all $\Sigma$-algebras together with their homomorphisms forms a category.

Instead of studying the structure of an algebra, we are going to study the structure of the collection of all algebras.

To remember the axioms of a category, it will be good to know that a monoid is also a category. In fact, as we will see, we can think of a category as a many-sorted, or typed, monoid.

Important parts of category theory are inspired by the fact that every order is also a category. But this perspective will not be exploited in this course.

Just a quick remark on monoids and orders as categories: I find it intriguing that category theory combines the two most common mathematical models for irreversible phenomena, monoids and orders, in one definition. [^self-reference]

[^self-reference]: Category theory is an axiomatic theory of strucure. But each category is also an example of mathematical structure. This self-reference plays an important role in various advanced areas.

## Axioms

We just list the definitions. It may be helpful to interleave reading the definitions with the examples of the next section.

### Category

One way to understand the definition of a category is as a "many-sorted" monoid. As we have seen in the first lecture, one can think of a monoid as a set of functions $f:A\to A$ closed under composition. Now we generalise this to $f:A\to B$ where the domain $A$ of $f$ and the codomain $B$ of $f$ are allowed to be different.

**Definition:** A **category** $\cal A$ consists of a collection of "objects" and for all objects $A,B\in \cal A$ a set $\cal A(A,B)$ of "arrows".

We write $f:A\to B$ for $f\in\cal A(A,B)$.

For all $A\in\cal A$ there is an "identity" arrow $id_A:A\to A$.

For all $A,B,C$ there is a "composition" operation $$\circ_{ABC}:{\cal A}(B,C)\times {\cal A}(A,B)\to {\cal A}(A,C)$$

We write $f\circ g=h$ for $\circ_{ABC}(f,g)=h$. The axioms are for all $h:A\to B$
\begin{gather*}
h\circ id_A = h = id_B\circ h
\end{gather*}
and for all $f:C\to D, g:B\to C$, $h:A\to B$
\begin{gather*}
(f\circ g)\circ h = f\circ (g\circ h)
\end{gather*}

**Exercise:** Show that a one-object category is exactly a monoid.

A category in which there is at most one arrow between any two objects is called a **thin category**.

**Exercise:** Show that a thin category is exactly an order (that is, a reflexive and transitive relation).

### Functor

A functor generalises the notion of monoid homomorphism from monoids to categories.

**Definition:** Let $\cal A, \cal B$ be two categories. A **functor**
$$F:\cal A\to\cal B$$

is a function from the objects of $\cal A$ to the objects of $\cal B$ and, for each pair $A,A'$ of objects of $\cal A$ a function
$$F_{AA'}:{\cal A}(A,A')\to{\cal B}(FA,FA')$$

that preserves identities and composition.

**Exercise:** Show that a functor betwee one-object category is exactly a monoid homomorphism. Similarly, a functor between thin categories is exactly an order preserving map.

**Exercise:** Show that `data List a = Nil | Cons a (List a)` in Haskell defines a functor. What other type constructors in Haskell are functors?

### Natural Transformations

We introduced categories and functors, but, so far, conceptually, we did not do anything remarkable from the point of view of mathematics. Indeed, catgories and functors are just a variation on a familiar theme that we illustrate with the table below.

|structure| morphism |
|:---:|:---:|
|monoid | monoid homomorphism |
| order | monotone map |
|graph | graph homomorphism |
|category | functor |

But now we will see the first definition that sets category theory apart. In fact, the story goes, categories and functors where discovered when Eilenberg and Mac Lane tried to capture the concept of a "natural map" mathematically. Technically, we extend the table above so that one obtains a good notion of "category of funtors". [^ccc]

|structure| morphism |
|:---:|:---:|
|functor | natural transformation |

[^ccc]: This remark goes beyond the scope of these lectures. One can axiomatise the set of all functions in category theoretic terms, obtaining the notion of a so-called cartesian closed category. The notion of natural transformation can be justified by the fact that it makes the category of categories a cartesian closed category.

**Definition:** Let $F,G:\cal A\to\cal B$. A **natural transformation** $$\tau:F\to G$$

is a parameterised collection $\tau_A:FA\to GA$ satisfying $Gf\circ \tau_{A} = \tau_{A'}\circ Ff$, or, in a picture,

...

for all $f:A\to A'$.

## More Examples

The paradigmatic examples of a category are
- the category of sets and functions and
- the category of types and programs

A large amount of category theory can be understood as an axiomatic characterisation of these two examples.[^twoexamples] So we look at these examples first. The other examples are less important for now, but illustrate that category theory reaches much further.

### Categories of types and programs

The example of types and programs is very closely related to the example of sets and function. For the purposes of this section the difference is only one of emphasis and perspective.

The operation
$$ (-)^\ast : Set\to Set$$

that maps an alphabet $X$ to the set $X^\ast$ of words over $X$ is a functor.

**Exercise:** Define $(-)^\ast$ on functions and verify that the laws of a functor are satisfied.

**Notation:** In work motivated in terms of programming languages this functor is often denoted by $\sf List$. In Haskell it is written using square brackets. Indeed, if `a` is a type, then `[a]` is the type of lists over `a`. To see this for yourself, head over to [`lists`](https://repl.it/@alexhkurz/lists#main.hs) and enter the following in the console:

:type reverse

`reverse` is a predefined function that reverses a list. The type of reverse is

reverse :: [a] -> [a]

Here, `a` is a type variable that can be instantiated with any type. Indeed, the algorithm for reversing a list does not depend on the type of the elements of the list.

Now it is easy to explain the idea behind the definition of a natural transformation:

- `reverse` is a natural transformation.
- Naturality is *exactly* the property that `reverse` can be implemented generically for all types of elements.

**Exercise:** Show that `reverse` is a natural transformation.

In programming languages terminology, naturality is an example of *parametric polymorphism*.

**Exercise:** What other examples of parametric polymorphic functions can you find?

We have just seen a first glimpse of type theory. There is a bit more in the homework below. Ask me if you want suggestions for further reading.

### Categories of sets

The category $Set$ has all sets as objects and all functions as arrows. (You may want to check that the axioms of a category are satsified.)

If this course was an introduction to category theory, we would now revisit definitions and construction that are defined in set-theory in terms of the elementship relation such as, for example, the cartesian product
$$ A\times B = \{(a,b) \mid a\in A, b\in B\}$$

Notice that this definition makes crucial use of $\in$. But the language of category theory only has $id$ and $\circ$.

So how can we define the product of two sets in the language of category theory?

In fact, and maybe surprisingly, it is possible to develop set theory in the language of category theory. Ask me if you want to know more about this. (This area of mathematics is known as **topos theory**.)

For now, we only need to feel the comfort of a familiar example. If in doubt of how to think of a category, just think in terms of sets and functions. [^thinkin]

[^thinkin]: There are interesting categories in which the "sets and functions" intuition is misleading. But we will not encounter them in this short introduction.

**Exercise:** Let $\mathcal PX$ be the set of subsets of $X$. For a function $f:X\to Y$, define $\mathcal Pf:\mathcal PX\to \mathcal PY$ as direct image, that is,
$$\mathcal P f(a)=\{f(x) \mid x\in a\}$$

for all $a\subseteq X$.[^directimage] Show that $\mathcal P$ is a functor.

There is an opportunity in the homework to pursue this a bit further.

### Categories of structures

Slogan: Mathematical structures of any kind organise themselves in a category.

The cateogy of
- monoids
- groups
- orders
- topological spaces
- ...

All of these categories are similar to the category of sets. We can think of the extra structure as eliminating some of the functions, namely those that are not structure preserving. Categories of structures are subcategories of the category of sets.

Categories of structures are the main topic of many introductory category theory books such as the ones by Mac Lane and by Adamek, Herrlich and Strecker.

### Categories of relations

What I mean here are categories where the arrows are not functions but relations. These categories have rather different properties than categories where arrows are functions.

Two prominent approaches to categories of relations are allegories and cartesian bicategories.

### Categories as structures

We have already seen two main examples: Every monoid is a category. Every order is a category. With some extra work one can also include metric spaces and variations into this picture.

The development of these ideas leads to enriched category theory.

### Categories as logical theories

In any reasonable logic there is a proof that $A$ implies $A$. We can think of this as the identity $id:A\to A$ in a category. Moreover, whenever I have a proof $f:A\to B$ and a proof $g:B\to C$ then there is a proof $f;g$ of $A\to C$.

From this point of view, a category is a logical theory and, vice versa, a logical theory is a category.

This idea turned out to be very fruitful. Categorical logic is a rich area of logic with close relations to topos theory, type theory, homotopy type theory.

## Theory

(if there is time ... a digression in some ways, but indispensable to better understand natural transformations, polymorphism, ... now delegated to one or two optional separate lectures)

Yoneda's lemma

Corollary: Every group is a group of permutations. Every monoid is a monoid of functions.

## Application

(I'd love to do this, but I think there will be no time and it is a digression anyway when the aim are monads ... moreover, before doing this one should spend some time on natural transformations)

Something from the theory of species.

Functors as mathematical structures up to isomorphism.

Deriving one example of a combinatorial formula.

## Homework

These exercises are about polymorphic functions/natural transformations.

The first exercise is, in my opinion, essential for a deeper understanding of category theory, but it can be skipped if one is interested mainly in the monad story.

### (Programming) Polymorphic Functions as Natural Transformations

From a programmer's point of view, implement as many functions of the types indicated in [`polymorphic`](https://repl.it/@alexhkurz/polymorphic#main.hs) as you can. From a mathematicians point of view try to characterise, for any given type, the set of *all* functions (considered as natural transformation between functors $Set\to Set$). It may be fewer functions than you think at first sight. [^a->a]

[^a->a]: For example, there is only one function/natural transformation of type `a->a`. There are only two functions/natural transformations of type `a->a->a`. Etc

### (Maths) Polymorphic Functions as Natural Transformations

This exercise is really the same as the previous one, now focussing more on the mathematics side than on the programming side.

**Exercise (Optional):** These exercises (in particular the 2nd and 4th) are more challenging. Try them if you want to learn more about category theory. If you just want the fastest route to monads, ignore them.

- Define for each function $A\to B$ a natural transformation $A\times X\to B\times X$.
- Show that each natural transformation $A\times X\to B\times X$ is induced by a function $A\to B$.
- Recall the definition of $X^A$ as the set of functions $A\to X$. Define for each function $B\to A$ a natural transformation $X^A\to X^B$.
- Show that each natural transformation $X^A\to X^B$ is induced by a function $B\to A$.

### (Maths) Sets as Quotients of Lists

The next exercise is one of the simplest examples of a natural transformation that is quotienting with respect to a set of equations. It illustrates that in mathematics there are functors and natural transformation that do not necessarily have an immediate implementation in a programming language.

Recall the definitions of the functors ${\sf List}$ and $\mathcal P$. Define a function
$${\sf List}(X)\to\mathcal PX$$

and show that is a natural transformation.

## Outlook

There is so much to say ... get in touch if you want to know more ... I may fill in sth later ...

## References and Further Reading

As a first introduction to category theory, I like the book "Conceptual Mathematics" by Lawvere and Schanuel but as far as I can see it is not available online. Neither is the classical "Categories for the Working Mathematician" by Mac Lane nor the monograph "Algebraic Theories" by Manes. But there is a lot of excellent material available.

The first book on category theory I read as a PhD student was

- Barr, Wells: [Category Theory for Computing Science](https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf).

I think it still is a very good introduction. A more advanced book, and an excellent source on toposes and monads (called triples there), is

- Barr, Wells: [Toposes, Triples and Theories](http://www.tac.mta.ca/tac/reprints/articles/12/tr12.pdf)

Another classic and important reference is

- Adamek, Herrlich, Strecker: [Abstract and Concrete Categories](http://katmat.math.uni-bremen.de/acc/acc.pdf).

More recent introductions to category, which I have not read myself, but which look very promising and commendable are

- Awodey: [Category Theory](http://scholar.google.com/scholar_url?url=https://www.researchgate.net/profile/Kameswara_Rao_Chellapilla2/post/Can_philosophy_help_to_innovate_and_develop_scientific_theory/attachment/5b632c2fb53d2f89289cfe85/AS%253A655211613933570%25401533226030818/download/Book_awodey__category_theory.pdf&hl=en&sa=X&ei=prgRYNHbLeaKywTa8IAg&scisig=AAGBfm3BlEpY04i0JDgo3_BlJZrtrYWafw&nossl=1&oi=scholarr)
- Leinster: [Basic Category Theory](https://arxiv.org/pdf/1612.09375)

An excellent book for learning more advanced category theory as it is used in modern mathematics is

- Riehl: [Category Theory in Context](https://people.math.rochester.edu/faculty/doug/otherpapers/Riehl-CTC.pdf)

[^twoexamples]: In fact, there is more than one category of sets and there is more than one category of types and programs. But we will have no time to pursue this further for now.

[^directimage]: A more widely used notation for $\mathcal Pf(A)$ is $f[A]$.