These are my lecture notes on Bartosz Milewski's course on category theory. These are not meant as a comprehensive guide but rather a loose collection of definitions and short summaries.

General stuff

A category is a collection of objects along with arrows, called morphisms, between those objects. It is therefore similar to a labeled directed graph.
A category has two properties: composition of morphisms and identity. Composition in category theory is similar to composition of functions and behaves associatively. Identity means that every object has an identity morphism.
Morphisms between any two objects form a set called the hom set denoted as \(hom(a, b)\). In higher-order categories morphisms don't form sets, they form objects in a category. A groupoid is a category in which every morphism has an inverse. A category whose objects form a set is called small, otherwise it's called large. An algebraic group is a category with a single object (corresponding to the set of elements of the group).


A morphism \(f: a \rightarrow b\) is called

Set

Set (capitalized) is the category of sets and functions. Set is a category because there is an identity function for each set which becomes the identity morphism in Set and function composition (which becomes morphism composition in Set) is associative.

In Set: surjective functions correspond to epimorphisms, injective functions correspond to monomorphisms and bijective functions correspond to bimorphisms.
Also notice the distinction between isomorphisms and bimorphisms. While in set theory a function that is bijective (both injective and surjective) is invertible, in category theory a bimorphism (which is both epic and monic) is not necessarily invertible (an isomorphism).

Category Theory in Programming

In a general sense, types in programming languages are sets:

If we go in the other direction we can ask which type in programming a specific set corresponds to:

The Empty Set

The empty set does not correspond to any type in most imperative languages, it does however correspond to the type Void in Haskell (omitting the bottom element).

We can define the following (uncallable) functions with Void in Haskell:
absurd :: Void → a
id_void :: Void → Void

The Singleton Set

The (one element) singleton set has one element called () and we can build the unit function with it:
unit :: a → ()

Furthermore we can define infinitely many functions of type () → a. These individual functions are constant. In this way we can express elements of a set as functions, or in category theory as morphisms.
For example for type bool we can define the functions
true :: () → Bool
true _ = True
false :: () → Bool
false _ = False
Here we have expressed the elements of the type set of Bool as morphisms.
Such an object () that allows us to view individual elements of a set as morphisms does not exist for every category. In general, category theory abstracts over elements and looks at sets, functions and other things from a higher perspective.

The two-element Set

(todo)

Sidenote: There is an important difference between pure functions in programming and mathematical functions. Mathematical functions instantly evaluate to a certain result while functions in programming may not terminate. To avoid this issue a special element called bottom is added to all type-sets above and a non-terminating function is said to return this bottom value.

Hask

Hask (capitalized) is the category of types and functions in Haskell (types include bottom). A mathematical function is only equivalent to a pure and total function in programming because it can't have side effects and is defined for every argument.