not representable (proof by haskell intuition).
type Hom a b = a -> b
type Nat f g = forall x. f x -> g x
class Representable f where
type Rep f :: *
tabulate :: forall x. ((Rep f -> x)) -> f x
index :: forall x. f x -> (Rep f -> x)
Stream is representable:
In general, things that are products tend to be representable, while things
that are sums tend not to.
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)
§ Every presheaf is a colimit of representables
Roughly, every presheaf can be written by "gluing" (union + equivalence relation/colimit)
functors of the form . Let 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 such that is the colimit of such a
set. Unwrapping what this means, it means that we have a functor such that
the image of is always a hom-set. That is, . Furthermore,
since is a colimit, we have arrows of the form . Recall that such an
arrow is a natural transformation between and . Also recall that by the Yoneda lemma,
such natural transformations are in natural bijection with elements in . So at some
point, we'll probably need to pick elements . 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 arrows
commute with image of the arrows in , of the form .
(2) that is the universal object in such that
this rats nest of hom-sets embeds perfectly into . Now the problem boils
down to designing a which picks out enough
hom-sets and relations between the hom-sets such that is the colimit of
such a .
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
, we need elements . Soo let's build a
category that does exactly that; This new category called as a Grothendieck construction.
Given a category and a presheaf , this new category called
has as objects pairs of the form . So we have a pair of an abstract object ,
and an element of its set , as , as is a presheaf, thus has the type .
The arrows in this category are derived from arrows in the original category .
Such an arrow lifts to a set-function thanks to the presheaf, . If we now have
, we can then build an arrow in which takes .
Picture speaks a thousand words:
So, this category gives us a way to "locate ourselves" within the set , which will be instrumental
in creating the arrows (natural transformations) of the form , as asked of us by the cocone.
This also hints at why we use colimis and not limits: because the yoneda goes from the to , we can only conjure
arrows into via Yoneda, thereby forcing us to use a colimit.
We claim that we should choose the diagram category as , with the diagram functor given
by . This embeds where is a way to locate 's
view of as a Hom-set . To give the natural transformation from the image of the diagram to the apex of the cocone ,
we use Yoneda: We need an arrow , which we know is in bijection with elements of through yoneda.
Luckily, we have to invoke yoneda, so we build the arrows from to ,
given by applying Yoneda to . 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 , with co-cone morphisms , we need to
create a natural transformation . Let's do this pointwise. for some ,
we need to build a map . Since the domain and codomain are pointwise,
let's pick some element . See that this can be seen as an element which is
an element of the category . But, recall that this was our index category . Thus, there is going
to be an arrow since is a cocone.
But since , it's an element of . We have thus found a way to map into
by "pulling back" into the index category and then "pushing forward" via Yoneda. [What the fuck is actually happening here?]
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))