§ Representable Functors


imagine image of functors F:CDF: C \rightarrow D, G:CDG: C \rightarrow D' as lying in sheets. Then a nautural transformation η\eta goes "perpendicular to these sheets. Often, knowing the natural transformation at one point determines it at every other point, if the category is rich-in-morphisms (eg. Set is very rich in morphisms). Now if we think of [C,Set][C, Set] (category of functors from CC to SetSet), we have all the Hom functors here, such as Hom(x,)Hom(x, -), Hom(y,)Hom(y, -), Hom(z,)Hom(z, -) etc. We may have some other functor F:CSet[C,Set]F: C \rightarrow Set \in [C, Set]. If this functor FF is isomorphic to some Hom-functor Hom(a,)Hom(a, -), then the functor FF is said to be a representable functor since it is represented by a single object aa through Hom(a,)Hom(a, -). PArametric polymorphism in haskell, that forces us to write one formula for all types makes these functions automatically natural transformations. So any implementation of a function such as foo :: Maybe a -> [a] will automatically be a nautral transformation (?)
Let's try and check if the list functor is representable. If I pick foo :: (Integer -> x) -> [x] this direction can be implemented as foo f = fmap f [0,1..]. On the other hand, the other way round does not work: foo:: [x] -> (Integer -> x) can't always be implemented. It's not representable (proof by haskell intuition).
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InstanceSigs #-}
type Hom a b = a -> b
type Nat f g = forall x. f x -> g x
class Representable f where
    type Rep f :: * -- the representing object o whose Hom(o, -) ~= f
    -- tabulate :: Nat (Hom (Rep f)) f
    -- tabulate :: forall x. Hom (Rep f) x -> f x
    tabulate :: forall x. ((Rep f ->  x)) -> f x
    -- index :: Nat f (Hom (Rep f))
    -- index ::  forall x. f x ->  (Hom (Rep f) x)
    index ::  forall x. f x ->  (Rep f -> x)



Stream is representable:
data Stream a = Cons a (Stream a)
instance Representable Stream where
   type Rep Stream = Integer
   tabulate i2x = go i2x 0 where
      go :: (Integer -> x) -> Integer -> Stream x
      go f i = Cons (f i) (go f (i+1))

   index :: Stream x -> Integer -> x
   index (Cons x xs) n = case n of 0 -> x; not0 -> index xs (n-1)

In general, things that are products tend to be representable, while things that are sums tend not to.

§ Every presheaf is a colimit of representables



Picture speaks a thousand words:
C | c -a→ d
Set | P(c) -P(a)→ P(d)
Set | u ∈ P(c) -P(a)→ d ∋ P(a)(u)
el P | (c∈C, u∈P(c))
el P | (c∈C, u∈P(c)) -el a→ (d∈C, P(a)(u)∈P(d))



§ Simplified construction of el(P)el(P)



              η
Hom(-, x) >------->P
   v               ^
   |arrow:        /
   | \h -> f.h   / μ
   v            /
Hom(-, y)>-----*