## § Representable Functors

imagine image of functors $F: C \rightarrow D$, $G: 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]$ (category of functors from $C$ to $Set$), we have all the Hom functors here, such as $Hom(x, -)$, $Hom(y, -)$, $Hom(z, -)$ etc. We may have some other functor $F: C \rightarrow Set \in [C, Set]$. If this functor $F$ is isomorphic to some Hom-functor $Hom(a, -)$, then the functor $F$ is said to be a representable functor since it is represented by a single object $a$ through $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: C \rightarrow Set$ can be written by "gluing" (union + equivalence relation/colimit) functors of the form $Hom(a_i, -)$. Let $P$ 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 \rightarrow [C, Set]$ such that $P$ is the colimit of such a set. Unwrapping what this means, it means that we have a functor $dgrm: J \rightarrow [C, Set]$ such that the image of $J$ is always a hom-set. That is, $dgrm(j \in J) = Hom(c_j, -) \in [C, Set]$. Furthermore, since $P$ is a colimit, we have arrows of the form $dgrm(j) = Hom(c_j, -) \rightarrow P$. Recall that such an arrow is a natural transformation between $Hom(c_j, -)$ and $P$. Also recall that by the Yoneda lemma, such natural transformations $Hom(c_j, -) \rightarrow P$ are in natural bijection with elements in $P(c_j)$. So at some point, we'll probably need to pick elements $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(c_j, -) \rightarrow P$ arrows commute with image of the arrows in $J$, of the form $Hom(c_j, -) \rightarrow Hom(c_{j'}, -)$. (2) that $P$ is the universal object in $[C, Set]$ such that this rats nest of hom-sets embeds perfectly into $P$. Now the problem boils down to designing a $dgrm: J \rightarrow [C, Set]$ which picks out enough hom-sets and relations between the hom-sets such that $P$ is the colimit of such a $dgrm$. 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(c_j, -) \rightarrow P$, we need elements $P(c_j)$. Soo let's build a category that does exactly that; This new category called as a Grothendieck construction. Given a category $C$ and a presheaf $P: C \rightarrow Set$, this new category called $el(P)$ has as objects pairs of the form $(c \in C, u \in P(c))$. So we have a pair of an abstract object $c \in C$, and an element of its set $u \in P(c)$, as $P(c) \in Set$, as $P$ is a presheaf, thus has the type $P: C \rightarrow Set$. The arrows in this category $el(P)$ are derived from arrows in the original category $c \xrightarrow{a} d$. Such an arrow lifts to a set-function thanks to the presheaf, $P(c) \xrightarrow{P(a)} P(d)$. If we now have $u \in P(c)$, we can then build an arrow in $el(C)$ which takes $(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)$, which will be instrumental in creating the arrows (natural transformations) of the form $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(c_j, -)$ to $P$, we can only conjure arrows into $P$ via Yoneda, thereby forcing us to use a colimit. We claim that we should choose the diagram category as $J\equiv el(P)$, with the diagram functor $dgrm: el(P) \rightarrow [C, Set]$ given by $dgrm(c \in C, u \in P(c)) : el(P) \equiv Hom(c, -) : [C, Set]$. This embeds $(c, u \in P(C))$ where $u$ is a way to locate $P$'s view of $C$ as a Hom-set $Hom(c -)$. To give the natural transformation from the image of the diagram to the apex of the cocone $P$, we use Yoneda: We need an arrow $Hom(c, -) \rightarrow P$, which we know is in bijection with elements of $P(c)$ through yoneda. Luckily, we have $u \in P(c))$ to invoke yoneda, so we build the arrows from $dgrm(c, u) = Hom(c, -)$ to $P$, given by applying Yoneda to $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 \in [C, Set]$, with co-cone morphisms $\sigma_j: Hom(c_j, -) \rightarrow Q$, we need to create a natural transformation $\theta: P \rightarrow Q$. Let's do this pointwise. for some $c \in C$, we need to build a map $\theta_c: P(c) \rightarrow Q(c)$. Since the domain and codomain are pointwise, let's pick some element $x \in P(c)$. See that this can be seen as an element $(c \in C, x \in P(c)$ which is an element of the category $el(P)$. But, recall that this was our index category $el(P)$. Thus, there is going to be an arrow $dgrm((c \in C, x \in P(c)) = Hom(c, -) \xrightarrow{q(c,x)} Q$ since $Q$ is a cocone. But since $q(c, x) \in [Hom(c, -), Q]$, it's an element of $Q(c)$. We have thus found a way to map $P(c)$ into $Q(c)$ by "pulling back" into the index category and then "pushing forward" via Yoneda. [What the fuck is actually happening here?]