This is a post going over the basic concept of defining objects through Universal Properties, in Category Theory, with explanations and examples in Haskell.

Universal Properties allow us to characterize objects not by their internal structure, or some kind of internal description, but in the unique way they relate to other things. This kind of description is powerful, because it shifts the focus from the content of each object, to how different objects relate to eachother. This is the focus of Category Theory more generally.

The Basics

The usual way of defining an object through a Universal Property goes something like this. You’re working in some category $\mathcal{C}$. You can characterize some universal object $U$ in terms of how it relates to other objects. Usually this means that you have a unique morphism into or out of $U$ making some kind of diagram commute.

You can think of this as saying that $U$ is the “best way” to solve some kind of problem.

I’m obviously being a bit vague here, but examples will follow shortly.

Initial

Let’s make this much more concrete. Our first universal object is that of an Initial Object. This object is characterized as follows:

An object $X$ is initial in $\mathcal{C}$ precisely when there exists a unique morphism $U \to A$ for every other object $A$ in $\mathcal{C}$.

We have some kind of diagram like this:

for any choice of $A$.

With $\bold{Set}$

Now, let’s make things even more concrete, and pick a specific category: $\bold{Set}$. This is the category with sets as objects, and normal functions as morphisms.

Does this category have an initial object?

Yes! $\emptyset$ is in fact the initial object. This is because we can define a function $\emptyset \to A$ for any other object $A$. A function $B \to C$ is really an assignment of a one element of $C$ for each element of $B$. If you pick $c \in C$ for each element $b \in B$, then you have a function. Since the empty set has no elements, we don’t have any choices to make, so we’re done!

In Haskell

There’s a “category” $\bold{Hask}$ of Haskell types and functions. You can basically take this category as being equivalent to $\bold{Set}$. Naturally, the “empty type” is going to be initial in $\bold{Hask}$:

data Void

This is the empty type, since there’s no way to construct it. How do we create a map to any other type?

absurd :: Void -> a
absurd _ = let a = a in a

Now, we cheat here by creating an infinite loop, but notice that it’s not actually possible to end up in the infinite loop. To do so, you’d have to produce a value of type Void, which is impossible!

Terminal

The dual notion to an initial object is a terminal object. Instead of having a unique map from our object. we have a unique map to our object:

In $\bold{Set}$, this object is the set with a single element: $\bullet := \{\bullet\}$.

Given some other set $A$, we define our unique map $f$ as:

$$ f(a) = \bullet $$

In Haskell

This translates straightforwardly to Haskell. Here, the type with a single element is (). Our universal map is defined in a similar way:

f :: a -> ()
f _ = ()

Uniqueness

Can there be more than one initial or terminal object?

Yes, but that object must be isomorphic to the initial / terminal object.

Let’s prove this for initial objects. Let’s say we have two objects $U, U'$ satisfying the initiality property.

We have unique maps $f : U \to U'$ and $f^{-1} : U \to U'$ between them. We can compose these to give us maps $f ; f^{-1} : U \to U$, and $f^{-1} ; f : U' \to U'$. But, the identity functions $1_U : U \to U$ and $1_{U'} : U' to U'$ are also maps. But, since any function out of $U$ or $U'$ must be unique, we have:

$$ \begin{aligned} f ; f^{-1} &= 1 \cr f^{-1} ; f &= 1 \cr \end{aligned} $$

which is precisely the condition for $f$ to be an isomorphism.

This can be summarized concisely by the following commutative diagram:

This proof can be reused almost piecemeal to show that terminal objects are unique up to isomorphism as well.

Universal Representation

The implication of this fact is that any representation of a type defined by a universal property is isomorphic.

For example, let’s take the terminal object (). We can represent this using the property itself!

data Terminal where
  Terminal :: forall a. a -> Terminal

Now, we’re using GADT syntax, because it makes this construction very clear. We have a function to convert an a into Terminal, given any type a. In practice, this is an existential type. Given an element of Terminal, we have some a, but we don’t know what type it actually had. It could have been anything.

Of course, since this encodes the universal property, it must be isomorphic to ():

iso1 :: Terminal -> ()
iso1 _ = ()

iso2 :: () -> Terminal
iso2 _ = Terminal ()

We can do the same trick for the initial object Void:

data Initial where
  Initial :: (forall a. a) -> Initial

We’d like to encode this as forall a. Initial -> a, but we have to settle for the less intuitive forall a. a. The idea is that given some instance of Initial, we have an element a, for any type of a.

As expected, we have an isomorphism:

iso1 :: Initial -> Void
iso1 (Initial v) = v

iso2 :: Void -> Initial
iso2 v = Initial (absurd v)

Products

The familiar product (a, b) is also characterized by a universal property! Notably, for any other type Z with projectors Z -> a, and Z -> b, there’s a unique morphism Z -> (a, b) making the following commute:

One way of thinking about this is that (a, b) is the simplest way of making a type that can project onto both a, and b. We have no extra information whatsoever. If we did have some extra information, say:

data User a b = User
  { name :: String,
    a :: a,
    b :: b
  }

We could always just pluck out the projections:

pluck (User _ a b) = (a, b)

We can define our “universal product” directly with the same technique’s we’ve seen earlier:

data Product a b where
  Product :: forall z. (z -> a) -> (z -> b) -> z -> Product a b

For any type z, if you have a projector to a and b, then you have a function z -> Product a b, by the universal property.

This is isomorphic to the standard product (a, b):

iso1 :: Product a b -> (a, b)
iso1 (Product fst' snd' z) = (fst' z, snd' z)

iso2 :: (a, b) -> Product a b
iso2 tuple = Product fst snd tuple

Sums

We can also encode the sum Either a b using a similar universal property. The definining characteristic of Either a b is that we can construct it from an a, or a b alone. Now, there might be other types that we can make with an a or a b, but Either a b is the simplest one.

Formally, for any other type z, with a constructor a -> z and b -> z, you have a function Either a b -> z, making the following diagram commute:

The intuition is the Either a b is the smallest type in which we can embed both elements of a and b. There might be larger types in which this embedding is possible, but we can always go through Either a b to make this embedding happen.

Using our standard trick, we can encode Either a b as a universal property

data CoProduct a b where
  CoProduct :: (forall z. (a -> z) -> (b -> z) -> z) -> CoProduct a b

In some sense, this type is the “opposite”, or dual to the Product we saw earlier, which is why it’s sometimes called the CoProduct.

Once again, it’s easy to show that an isomorphism exists:

iso1 :: CoProduct a b -> Either a b
iso1 (CoProduct f) = f Left Right 

iso2 :: Either a b -> CoProduct a b
iso2 (Left a) = CoProduct (\l _ -> l a)
iso2 (Right b) = CoProduct (\_ r -> r b)

Conclusion

This was just a quick post to go over the basics of objects defined using universal properties, along with some examples of encoding them in Haskell.

The main weakness of this approach is that we can’t capture properties that aren’t structural. For example, we have a functions $f : A \to W$, and $g : B \to W$, and we want to find the subset of the product $(A, B)$, such that $\pi_A : f = \pi_B : g$ (this is called the pullback), then our universal representation fails to capture this property, since this isn’t encoded structurally.

Anyways, there’s a lot more to explore, but I wanted to get some of the basics out there in a quick post.