`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.
- 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))$.

```
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? ]

- Recall that $el(P)$ consisted of a pair $(c \in C, u \in P(c))$. We know from Yoneda that set elements of $P(c)$ are in bijection with natural transformations $eta_c: Hom(-, c) \to P$.
- Thus $el(P)$ consists of
*all*natural transformations $\eta_c: Hom(-, c) \Rightarrow P$ [for all objects $c$]. - The arrows in $el(P)$ between $\eta: Hom(-, x) \Rightarrow P$ and $\mu: Hom(-, y) \Rightarrow P$ are pushforwards of arrow $x \xrightarrow{f} y$ (given by $\lambda h. f \circ h$) which make the diagram commute:

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

- Consider the functor $J: el(P) \to [C^{op}, Set]$ which sends each natural transformation $\eta:Hom(-, x) \Rightarrow P$ to just $J(\eta: Hom(-, x) \Rightarrow P) \equiv Hom(-, x)$ (ie, forget the mapping, just keep the domain of the natural transformation.
- We claim that $P$ is the cocone of the functor $J$. So we must have mappings from each $Hom(c, -)$ into $P$.
- These mappings from $Hom(c, -)$ into $P$ are given by "un-forgetting" the data we forgot when mapping $\eta:Hom(-, c) \Rightarrow P \mapsto Hom(-, c)$. These commute by the construction of $el(P)$.
- (Are these the only choices of maps? Maybe there are others, not just the ones we "un-forgot"!)
- Next we need to check that $P$ is universal. Consider some other $Q: C^{op} \Rightarrow Set$. We must show a map $\alpha: P \Rightarrow Q$(ie, the cocone $Q$ factorizes through $P$, or $P$ is initial cocone.).
- Let's do this pointwise. So we want to define a family $\alpha_k: P(k) \Rightarrow Q(k)$.
- Pick some element $e \in P(k)$. This corresponds to some natural transformation $\eta_e: Hom(-, k) \rightarrow P$. We know that we have a corresponding $\eta_e': Hom(-, k) \rightarrow Q$. this is some element $e' \in Q(k)$. So we are forced to set $e \mapsto e'$ when we try to map $P(k)$ to $Q(k)$.
- This works for arbitrary $k, e$, so the entire map is determined. This proves that $P$ is terminal cocone.

- Reference
- Density theorem proof #Proof)