Fun with Functors

In our last post we provided some examples of categories which show how, with our newly defined concept of category, we can generalize a lot of already well known mathematical structures.

We understood how a category gives us a context where we can talk about composition, being assured that the desired properties as identity and associativity hold. But sometimes, we would like to be able to jump from one context to another, making connections between the two. But what does this mean? When is a connection between two contexts meaningful? The answer a category theorist could give is that a connection between two contexts is meaningful when the invariants present in our starting context are preserved by the connection itself.

In the world of category theory, these connections are represented by functors, which provide ways to go from one category to another respecting the categorical structure.

What is a functor

Simply stated, a functor is a mapping between categories which preserves their structure, but let us see what this means in all its details.

First thing, a functor goes between two categories, which we will call cat1 and cat2, and we can start defining it in Idris as

record Functor (cat1 : Category) (cat2 : Category) where

Now we want to define how our functor acts on cat1. Remember that a category is composed by objects and morphisms, so we will need to define how Functor acts on both. Let us start with objects:

mapObj : obj cat1 -> obj cat2

We simply have a function, which we call mapObj, which provides a way to map objects of cat1 into objects of cat2.

http://yannesposito.com/Scratch/fr/blog/Category-Theory-Presentation/

For morphisms, we don’t want to have just a function that maps a morphism of cat1 to a generic morphism of cat1, but we want to impose some coherence conditions on the source and the target of the mapped morphism. This amounts to say that, if we have a morphism a -> b in cat1, then we would like to map it to a morphism mapObj a -> mapObj b, respecting the action of mapObj on the objects of cat1.

mapMor : (a, b : obj cat1)
      -> mor cat1 a b
      -> mor cat2 (mapObj a) (mapObj b)

To make this explicit we add to our Functor record a mapMor function which tells how, for any two objects a and b of cat1, we can map a morphism between a and b to a morphism, this time in cat2, between mapObj a and mapObj b.

http://yannesposito.com/Scratch/fr/blog/Category-Theory-Presentation/

It is probably the case to stress here that in general, in category theory mapObj and mapMor are indicated with the same symbol, because it is possible to distinguish between the two usages just by checking if their argument is an object or a morphism. But, since here we are actually trying to explain category theory to the Idris compiler, we are required to be extremely pedantic and precise, so we need to use two different symbols.

Are we done now, since we can map objects and morphisms? Don’t be in such a hurry, we have mapped only the bare structure, but that’s not all there is to a category. Actually, probably the main important idea laying around in a category is the one of composition, so when defining a functor we really need to ensure that we are preserving composition too.

preserveCompose : (a, b, c : obj cat1)
               -> (f : mor cat1 a b)
               -> (g : mor cat1 b c)
               -> mapMor a c (compose cat1 a b c f g)
                = compose cat2
                          (mapObj a)
                          (mapObj b)
                          (mapObj c)
                          (mapMor a b f)
                          (mapMor b c g)

We introduce a new field preserveCompose in our Functor record which tells us that for any objects a, a and c and morphisms f : a -> b and g: b-> c of cat1, we obtain the same result if we do on of the following:

• compose f and g in cat1 and then map the result with mapMor
• map f and g into cat2 using mapMor and then compose the results in cat2

In other words, we can say that we can swap the order of composition and functor application, or better yet, that functor application preserves composition.

Composition in a category actually comes also with the concept of identity, so a functor needs to preserve that too.

preserveId : (a : obj cat1)
          -> mapMor a a (identity cat1 a)
           = identity cat2 (mapObj a)

This condition tells us that, given any object a of cat1, the identity morphisms of a is mapped by mapMor to the identity morphism, this time in cat2, of mapObj a, as one would expect.

Examples of functors

Now that we have a complete definition of a functor, it is time to see some concrete examples, investigating what functors are in the categories we introduced in our previous post.

Discrete categories

As we discussed last time, discrete categories are categories where the only morphisms are the identities of the objects. This means that, in practice, we can’t talk about composition in discrete categories. Everything is isolated in its own world. As a consequence, when defining a functor between discrete categories, we don’t need to bother with how mapMor will work, because it will even send only identities to identities, but we can concentrate only on mapObj.

Actually, if we cave two discrete categories cat1 and cat1, which sets of objects are respectively object cat1 and object cat2, every function f : object cat1 -> object cat2 defines a functor. We can actually prove it as follows:

functionMapMor :
     (f : a -> b)
  -> (x, y : a)
  -> DiscreteMorphism x y
  -> DiscreteMorphism (f x) (f y)
functionMapMor f x x Refl = Refl
functionPreserveCompose :
     (f : a -> b)
  -> (x, y, z : a)
  -> (g : DiscreteMorphism x y)
  -> (h : DiscreteMorphism y z)
  -> functionMapMor f x z (discreteCompose x y z g h)
   = discreteCompose (f x)
                     (f y)
                     (f z)
                     (functionMapMor f x y g)
                     (functionMapMor f y z h)
functionPreserveCompose f x x x Refl Refl = Refl
functionAsFunctor :
     (f : a -> b)
  -> CFunctor (discreteCategory a) (discreteCategory b)
functionAsFunctor f = MkCFunctor f
                                 (functionMapMor f)
                                 (\_ => Refl)
                                 (functionPreserveCompose f)

Monoids

We know that a monoid could be seen as a degenerate category with only one object, where the composition in the category is nothing else than the binary operation of the monoid and the identity morphism is the identity element of the monoid.

What about functors between such categories? Suppose we want to define a functor between categories monoidAsCategory monoid1 and monoidAsCategory monoid2; well, we don’t have a lot of choice for mapObj, we need to map the only object of the starting category to the only object of the target category. For mapMor, we need to map morphisms of monoidAsCategory monoid1 to morphisms of monoidAsCategory monoid2; but morphisms in these categories are just elements of the respective monoids. Therefore we need a function fun from monoid1 to monoid2. Moreover, for it to be the morphism component of a functor, we need it to respect composition and the identity morphism; but this amounts exactly to say that fun must be a monoid homomorphism! We can actually prove that for every monoid homomorphism between monoids monoid1 and monoid2, we can build a functor between their associated categories monoidAsCategory monoid1 and monoidAsCategory monoid2.

record MorphismOfMonoids domain codomain where
  constructor MkMorphismOfMonoids
  func : domain -> codomain
  funcRespOp :
       (VerifiedSemigroup domain, VerifiedSemigroup codomain)
    => (a, b : domain)
    -> FunctionRespectsOperation a b func
funcRespId :
       (VerifiedMonoid domain, VerifiedMonoid codomain)
    => FunctionRespectsIdentity func
morphismOfMonoidsToFunctor :
     (monoid1, monoid2 : Monoid)
  -> MorphismOfMonoids monoid1 monoid2
  -> CFunctor (monoidAsCategory monoid1)
              (monoidAsCategory monoid2)
morphismOfMonoidsToFunctor
  monoid1
  monoid2
  (MkMorphismOfMonoids fun frOp frId) =
MkCFunctor
  id
  (\_, _ => fun)
  (\_ => frId)
  (\_, _, _, f, g => frOp f g)

Preorders

Let us recall that a preorder can be seen as a category with at most one morphism between any two objects, where the order structure is reflected in the presence or absence of a morphism.

Now, how does a functor between two such categories cat1 = preorderAsCategory {t1} {po1} and cat2 = preorderAsCategory {t2} {po2}, where po1 and po2 are partial orders respectively on t1 and t2, look like? It is constituted by a function f between mapObj cat1 = t1 and mapObj cat2 = t2 and, for any objects a and b, a function between mapMor cat1 a b = po1 a b and mapMor cat2 a b = po2 a b; since in these categories there is at most one morphism between any two objects a and b, the latter function can be interpreted by saying that if there is a morphism a -> b, there must exists a morphism f a -> f b. Translating this in preorder terms, this amounts to saying that a <= b in po1 implies f a <= f b in po2. This shows that functors between preorder categories are nothing else than order preserving functions! Let’s show in Idris that any order preserving function can be seen as a functor:

record MonotoneMap
  (t1 : Type)
  (po1 : t1 -> t1 -> Type)
  (t2 : Type)
  (po2 : t2 -> t2 -> Type)
where
  constructor MkMonotoneMap
  func : t1 -> t2
  funcRespOrd : (a, b : t1) -> po1 a b -> po2 (func a) (func b)
  
monotoneMapToFunctor :
     (UniquePreorder t1 po1, UniquePreorder t2 po2)
  => MonotoneMap t1 po1 t2 po2
  > CFunctor (preorderAsCategory {t = t1} {po = po1})          
            (preorderAsCategory {t = t2} {po = po2})
monotoneMapToFunctor
  {t1}
  {po1}
  {t2}
  {po2}
  (MkMonotoneMap fun fRespectsOrd) =
MkCFunctor
  fun
  fRespectsOrd
  (\a => unique (fun a)
                (fun a)
                (fRespectsOrd a a (reflexive a))
                (reflexive (fun a)))
  (\a, b, c, f, g =>
    unique (fun a)
           (fun c)
           (fRespectsOrd a c (transitive a b c f g))
           (transitive (fun a)
                       (fun b)
                       (fun c)
                       (fRespectsOrd a b f)
                       (fRespectsOrd b c g)))

Recall that reflexive and transitive are the functions associated with the Preorder interface, while unique comes from the UniquePreorder interface we introduced in our last post.

Notice also how the preservation of the identity morphisms and of composition follow directly from the fact that there is at most one morphism between two objects. To prove that two morphisms are equal it is then enough to observe that they have the same origin and the same target.

Conclusion

Functors are our precise way of defining a change of context where information is preserved. Whenever in your mind you make a nice connection between two different worlds, and there is some kind of preservation of structure, it is really probable that you could express your thought formally in terms of categories and functors!

In our last post we introduced three classes of categories, respectively discrete categories and categories associated to monoids and to preorders. Today we observed that functors between such categories are exactly structure preserving morphisms between those objects. In the case of monoids, the operational structure is preserved; in preorders, functors are order preserving morphisms; in discrete categories, there’s no structure to preserve, so any function is fine!

If you know a bit of functional programming and have been playing around with Haskell or Idris, you will probably know that there is already a concept of Functor defined in the language. How does it relate with what we defined today? That’s exactly the question we will tackle in our next post!