Natural Tranformation in a More General Context

Question

I've been building my way up through some category theory in Haskell on my way to creating more general Monads.

Before I can move onto the next step I am going to need to be able to work with natural transformations.

Now natural transformations on regular Functors are easy enough they are just functions

trans :: forall a . F a -> G a

(where F and G are Functors) with the additional restriction that

fmap f . trans = trans . fmap f

equivalent to the commutative diagram:

However when I move on to more categorical functors

class
  ( Category cat1
  , Category cat2
  )
    => Functor cat1 cat2 f
  where
    map :: cat1 a b -> cat2 (f a) (f b)

I am not sure how I can augment the definition of natural transformation to keep up.

The diagram implies that

trans :: forall a . cat2 (F a) (G a)

where

Functor cat1  cat2 F
Functor cat1' cat2 G

However it is not clear to me that it must be the case that cat1 ~ cat1'. Or what the relationship between the transformation and the precategories of both functors are.

What does a natural tranformation look like in the broader context of Haskell Functors over more general categories?

user_6863749 · Answer

However it is not clear to me that it must be the case that cat1 ~ cat1'.

It's part of the definition of a natural transformation that the functors F and G have the same domain and codomain. From nlab:

Given categories C and D, and functors F, G : C -> D

So a direct translation of the definition in Haskell is that a natural transformation between functors F, G with domain cat1 and codomain cat2 is as a polymorphic term, a family of morphisms cat2 (F a) (G a) indexed by objects a:

n :: forall a. cat2 (F a) (G a)

such that a certain diagram commutes for all f :: cat1 a b, i.e., we have the following equation, where (.) is composition in cat2:

fmap f . n = n . fmap f

where n is specialized at type a on the left, and at type b on the right.

Note that this encoding is limited in expressiveness, because Haskell forall is not identical to English "for all". The behavior of n :: forall a. ... cannot really depend on a. forall implies a form of "uniformity" (aka. parametricity) which is not found in the definition of "natural transformations".

Natural Tranformation in a More General Context

1 Answers