§ 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

Roughly, every presheaf P:CSetP: C \rightarrow Set can be written by "gluing" (union + equivalence relation/colimit) functors of the form Hom(ai,)Hom(a_i, -). Let PP be the presheaf. To say that it can be written as a colimit of Hom-sets, this means that we have some (yet unknown) diagram dgrm:J[C,Set]dgrm: J \rightarrow [C, Set] such that PP is the colimit of such a set. Unwrapping what this means, it means that we have a functor dgrm:J[C,Set]dgrm: J \rightarrow [C, Set] such that the image of JJ is always a hom-set. That is, dgrm(jJ)=Hom(cj,)[C,Set]dgrm(j \in J) = Hom(c_j, -) \in [C, Set]. Furthermore, since PP is a colimit, we have arrows of the form dgrm(j)=Hom(cj,)Pdgrm(j) = Hom(c_j, -) \rightarrow P. Recall that such an arrow is a natural transformation between Hom(cj,)Hom(c_j, -) and PP. Also recall that by the Yoneda lemma, such natural transformations Hom(cj,)PHom(c_j, -) \rightarrow P are in natural bijection with elements in P(cj)P(c_j). So at some point, we'll probably need to pick elements P(cj)P(c_j). We're not done yet, this is what one part of what it means to be a colimit; we also need all the diagrams to commute! (1) the embedding natural transformations Hom(cj,)PHom(c_j, -) \rightarrow P arrows commute with image of the arrows in JJ, of the form Hom(cj,)Hom(cj,)Hom(c_j, -) \rightarrow Hom(c_{j'}, -). (2) that PP is the universal object in [C,Set][C, Set] such that this rats nest of hom-sets embeds perfectly into PP. Now the problem boils down to designing a dgrm:J[C,Set]dgrm: J \rightarrow [C, Set] which picks out enough hom-sets and relations between the hom-sets such that PP is the colimit of such a dgrmdgrm. The idea, once, again, goes back to (a) Yoneda, and (b) Grothendeick. It appears that to be able to pick out such embedding arrows for the co-cone Hom(cj,)PHom(c_j, -) \rightarrow P, we need elements P(cj)P(c_j). Soo let's build a category that does exactly that; This new category called as a Grothendieck construction. Given a category CC and a presheaf P:CSetP: C \rightarrow Set, this new category called el(P)el(P) has as objects pairs of the form (cC,uP(c))(c \in C, u \in P(c)). So we have a pair of an abstract object cCc \in C, and an element of its set uP(c)u \in P(c), as P(c)SetP(c) \in Set, as PP is a presheaf, thus has the type P:CSetP: C \rightarrow Set. The arrows in this category el(P)el(P) are derived from arrows in the original category cadc \xrightarrow{a} d. Such an arrow lifts to a set-function thanks to the presheaf, P(c)P(a)P(d)P(c) \xrightarrow{P(a)} P(d). If we now have uP(c)u \in P(c), we can then build an arrow in el(C)el(C) which takes (cC,uP(c))el(P)(a)(dC,P(a)(u)P(d))(c \in C, u \in P(c)) \xrightarrow{el(P)(a)} (d \in C, P(a)(u) \in P(d)). 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))
So, this category gives us a way to "locate ourselves" within the set P(c)P(c), which will be instrumental in creating the arrows (natural transformations) of the form Hom(cj,)P(cj)Hom(c_j, -) \rightarrow P(c_j), as asked of us by the cocone. This also hints at why we use colimis and not limits: because the yoneda goes from the Hom(cj,)Hom(c_j, -) to PP, we can only conjure arrows into PP via Yoneda, thereby forcing us to use a colimit. We claim that we should choose the diagram category as Jel(P)J\equiv el(P), with the diagram functor dgrm:el(P)[C,Set]dgrm: el(P) \rightarrow [C, Set] given by dgrm(cC,uP(c)):el(P)Hom(c,):[C,Set]dgrm(c \in C, u \in P(c)) : el(P) \equiv Hom(c, -) : [C, Set]. This embeds (c,uP(C))(c, u \in P(C)) where uu is a way to locate PP's view of CC as a Hom-set Hom(c)Hom(c -). To give the natural transformation from the image of the diagram to the apex of the cocone PP, we use Yoneda: We need an arrow Hom(c,)PHom(c, -) \rightarrow P, which we know is in bijection with elements of P(c)P(c) through yoneda. Luckily, we have uP(c))u \in P(c)) to invoke yoneda, so we build the arrows from dgrm(c,u)=Hom(c,)dgrm(c, u) = Hom(c, -) to PP, given by applying Yoneda to uP(c)u \in P(c). Thus, we can at least form a cocone. Whether the arrows of the base of the cocone commute with the apex-pointing arrows, and whether this is universal is to be checked next. Given some other cocone Q[C,Set]Q \in [C, Set], with co-cone morphisms σj:Hom(cj,)Q\sigma_j: Hom(c_j, -) \rightarrow Q, we need to create a natural transformation θ:PQ\theta: P \rightarrow Q. Let's do this pointwise. for some cCc \in C, we need to build a map θc:P(c)Q(c)\theta_c: P(c) \rightarrow Q(c). Since the domain and codomain are pointwise, let's pick some element xP(c)x \in P(c). See that this can be seen as an element (cC,xP(c)(c \in C, x \in P(c) which is an element of the category el(P)el(P). But, recall that this was our index category el(P)el(P). Thus, there is going to be an arrow dgrm((cC,xP(c))=Hom(c,)q(c,x)Qdgrm((c \in C, x \in P(c)) = Hom(c, -) \xrightarrow{q(c,x)} Q since QQ is a cocone. But since q(c,x)[Hom(c,),Q]q(c, x) \in [Hom(c, -), Q], it's an element of Q(c)Q(c). We have thus found a way to map P(c)P(c) into Q(c)Q(c) by "pulling back" into the index category and then "pushing forward" via Yoneda. [What the fuck is actually happening here?]