Can we define the Functor Category in Haskell (or any other language with a more expressive type system)?
Ed Kmett has actually defined this in his Hask library. The trick is to define a natural transformation as a data type and encoding the functors that this natural transformations map, in the type level like this:

class (Functor f, Dom f ~ p, Cod f ~ q) =&gt; FunctorOf p q f
instance (Functor f, Dom f ~ p, Cod f ~ q) =&gt; FunctorOf p q f


data Nat (p :: i -&gt; i -&gt; *) (q :: j -&gt; j -&gt; *) (f :: i -&gt; j) (g :: i -&gt; j) where
  Nat :: ( FunctorOf p q f
         , FunctorOf p q g
         ) =&gt; {
           runNat :: forall a. Ob p a =&gt; q (f a) (g a)
         } -&gt; Nat p q f g


Now he defines the Natural transformation as instances of a Category like this:

instance (Category' p, Category' q) =&gt; Category' (Nat p q) where
   type Ob (Nat p q) = FunctorOf p q
   id = Nat id1 where
     id1 :: forall f x. (Functor f, Dom f ~ p, Cod f ~ q, Ob p x) =&gt; q (f x) (f x)
     id1 = id \\ (ob :: Ob p x :- Ob q (f x))
   observe Nat{} = Dict
   Nat f . Nat g = Nat (f . g)
   unop = getOp


All of this can be found here: https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs