A Universe of Sorts

§ 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

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

§ Simplified construction of $el(P)$

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)

§ Representable Functors

§ Every presheaf is a colimit of representables

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

§ Simplified construction of $el(P)$