Concrete Categories

In our first post on categories in Idris we provided a definition of category which we can practically use. But we didn’t actually check with any examples if that definition is a good one, meaning that we can easily work with it. That’s exactly what we are here for today: we will introduce a few easy examples of categories and we will implement them in Idris.

Let’s get started with the easiest class of categories one could think of.

Discrete categories

When we introduced the idea of category, the first component we presented were objects. We can think about them as a bunch of dots scattered around. So let’s start from a generic collection of objects, represented by a type a : Type in Idris, and try to build the smallest possible category on top of it. In other terms, we need to fill the holes in the following definition

discreteCategory : (a : Type) -> Category
discreteCategory a = MkCategory
  a
  ?mor
  ?id
  ?comp
  ?lId
  ?rId
  ?assoc

https://de.wikipedia.org/wiki/Datei:Discrete_category.svg

The first hole asks us which should be the morphisms between any two objects x : a and y: a. By the definition of a category, we know that we must have at least the identity morphism going from any object x to itself. Since we want to build the smallest possible category with objects in a, we start by adding only these morphisms, and we check if they are enough to form a category. So we define

DiscreteMorphism : (x, y : a) -> Type
DiscreteMorphism x y = x = y

This means that, for any objects x : a and y: a, the collection of objects will be given by all the proofs that x is equal to y. Clearly, if x and y are distinct objects, there is no proof of their equality, so the collection DiscreteMorphism x y will have no elements. On the other hand, if x and y are the same object, in Idris we have one and only one inhabitant of the type x = x, called Refl. Here, notice that in type theory in general it’s not always true that two elements of x = x need to be equal; if you want to know more about this, have a look at Homotopy type theory.

Our above discussion clarifies already that the only possible choice we have for the identity morphism for a generic object x is Refl : DiscreteMorphism x x

discreteIdentity : (x : a) -> DiscreteMorphism x x
discreteIdentity _ = Refl

Only composition is left among the basic elements to define a category. To define it, we need to consider three objects x, y and z and two morphisms f : x -> y and g: y -> z. But we don’t have many morphisms around, and we can use this fact at our advantage! Since the only morphisms are identity morphisms, both f and g must be identity morphisms, and therefore x must be equal to y and y must be equal to z. By transitivity of equality, it follows that x must be equal to z, and so there is a morphism from x to z, i.e. the identity of x = y = z, which we define to be the composition of f and g. In Idris terms we can write this as

discreteCompose : (x, y, z : a)
               -> (f : DiscreteMorphism x y)
               -> (g : DiscreteMorphism y z)
               -> DiscreteMorphism x z
discreteCompose _ _ _ Refl Refl = Refl

At this point we have all we need to prove the laws to check that what we are defining is indeed a category. We’re only going to discuss the first one, regarding left identity, and we leave the other two to the reader (you’re welcome to post your solutions in the comments, if you want!).

The left identity law asserts that whenever we compose an identity morphism with a morphism f, what we obtain is exactly f. Since in our setting we have only identity morphisms, this amounts to say that the composition of two identity morphisms, on the same object x, is again the identity on x. But this is always true.

discreteLeftId : (x, y : a)
              -> (f : DiscreteMorphism x y)
              -> discreteCompose x x y (discreteIdentity x) f = f
discreteLeftId _ _ Refl = Refl

Preorders

Now let’s try to relax a bit… discrete categories are nice but they are kind of too poor on structure; we would like to have some more morphisms! What we can do is allow the presence of morphisms between any two objects; but wait, not as many as you’d like! Let’s start by adding at most one morphism between any two objects.

In fact, categories which satisfy this properties correspond exactly to preorders, where a preorder is a set X with a binary relation ≤ satisfying the following properties:

• reflexivity: x ≤ x for any element x of X
• transitivity: if x ≤ y and y ≤ z, then x ≤ z

Let’s see how we can implement the proof that any preorder can be interpreted as a category with at most one morphism between any two objects. Idris already has a definition of Preorder which can be found in the Decidable.Order module

interface Preorder t (po : t -> t -> Type) where
  reflexive : (a : t) -> po a a
  transitive : (a : t)
            -> (b : t)
            -> (c : t)
            -> po a b
            -> po b c
            -> po a c

where t is the type of elements of the preorder and po is the ≤ relation on t. What we want is to obtain a category starting from a preorder

preorderAsCategory : Preorder t po => Category

It is natural to choose t as type of the objects of the category and po as the type of morphisms. Identity morphisms are provided by the reflexive axiom and composition is given by transitivity. To see that this works as expected, just try to visualize the ≤ as arrows -> going from smaller elements to greater ones.

Now we are left with proving the laws. As we did above, we’re going to concentrate only on the left identity and leave the other two to the reader. What we need to prove is that, for any two elements a : t and b: t and a proof f : po a b that a ≤ b, then composing f with the identity of a should give us back f itself. In terms of preorders this amounts to saying that using the transitivity property with a ≤ a and a ≤ b should tell us that a ≤ b. This reads kind of obvious, but in fact we’re not able to prove it in Idris! This is due to the fact that the axioms we have for Preorder at the moment are not concerned with equality of terms of type po a b, or even less with their uniqueness. Hence, to complete our proof, we need to add a new axiom to state explicitly that there is at most one proof that a ≤ b, or, in other terms, all the proofs that a ≤ b are equal

interface Preorder t po => UniquePreorder t (po : t -> t -> Type)              
  where
    unique : (a, b : t) -> (f, g : po a b) -> f = g

We do it by extending the Preorder interface with a new function unique which allows us to assert that any two f, g : po a b must actually be equal. This allows us to prove that

leftIdentity : UniquePreorder t po
  => (a, b : t)-> (f : po a b)
  -> transitive a a b (reflexive a) f = f
leftIdentity a b f
  = unique a b (transitive a a b (reflexive a) f) f

With analogous proofs for rightIdentity and associativity, we can conclude our proof that a preorder can be seen as a category

preorderAsCategory : UniquePreorder t po => Category
preorderAsCategory {t} {po} = MkCategory
  t
  po
  reflexive
  transitive
  (leftIdentity {t} {po})
  (rightIdentity {t} {po})
  (associativity {t} {po})

Monoids

There is another class of categories that we can find among the common algebraic data structures. For preorders, we imposed on our category a restriction on the number on morphisms. Let’s try now to impose a restriction on the number on objects and consider a category which has only one object a (there is also a category with zero objects and zero morphisms, but it’s not that interesting!).

https://en.wikiversity.org/wiki/File:Generators_of_free_monoid.svg

We know that we have the identity morphism e : a -> a and that for any pair of morphisms f : a -> a and g : a -> a we have another morphism f ; g which is their composition. Moreover, the following rules need to be satisfied:

• identity: for any f : a -> a we have f ; e = f = e ; f
• associativity: for any f, g, h : a -> a we have f ; (g ; h) = (f ; g) ; h

This amounts exactly to saying that the collection of morphisms a -> a form a monoid.

We can actually prove in Idris that, given any monoid, we can construct a category which has only one object and that monoid as a set of morphisms on that object.

MonoidMorphism : (monoid : Type) -> Unit -> Unit -> Type
MonoidMorphism monoid _ _ = monoid
monoidAsCategory : VerifiedMonoid monoid => Category
monoidAsCategory {monoid} = MkCategory
  Unit
  (MonoidMorphism monoid)
  (\_ => neutral)
  (\_, _, _, f, g => f <+> g)
  (\_, _, f => monoidNeutralIsNeutralR f)
  (\_, _, f => monoidNeutralIsNeutralL f)
  (\_, _, _, _, f, g, h => semigroupOpIsAssociative f g h)

where Unit is the type which has only one element, neutral is the identity element of the monoid, <+> is the operation of the monoid and monoidNeutralIsNeutralR, monoidNeutralIsNeutralL and semigroupOpIsAssociative are the axioms of the monoid stating that neutral is actually a left and right identity and that the operation is associative.

Conclusion

In this post we saw that we can interpret some well known algebraic structures as orders and monoids in a categorical context. This means that a category generalizes both the concept of a preorder and the concept of a monoid, providing a more general setting where we can unify a lot of known mathematical ideas.

As a side note, it is interesting that, for any category C, we can obtain a preorder by defining an order on the set of objects by a ≤ b if there exists a morphism from a to b. Moreover, for any object a of C, the set of morphisms from a to a (called also endomorphisms) always form a monoid.

Now that we obtained several examples of categories, we could ask ourselves how we can connect them, to establish relation between them. Isn’t category theory a way of studying and analysing connections between entities, after all? That’s exactly what we’re going to do in our next post, where we’ll talk about functors.