For later. Yoneda.

gistfile1.txt

00:34 <edwardk> spacekitteh: not in 30 seconds or less ;)
00:37 <edwardk> but the short version of it is that if you take a category, and look at its hom-sets C^op * C -> Set and fix its second argument, so you are looking at the space of all arrows into an object, these spaces of arrows are what we call presheaves (functors from C^op -> Set) the yoneda embedding Y : C -> [ C^op, Set ] is the functor that takes objects in C to their corresponding presheaves in this way.
00:38 <edwardk> why is that interesting?
00:39 <edwardk> well, if you look the functor category [X, Y] of functors from X to Y with natural transformations between them as your arrows then you can find that this category inherits most of its structure from Y.
00:40 <edwardk> [2, Set] is Set^2, its basically pairs of objects for objects, pairs of arrows for arrows, it is cartesian because Set is cartesian, it is cocartesian because set is cocartesian, etc.
00:40 <edwardk> that suggests that [C^op, Set] acts a lot like Set!
00:40 <benl23> CCC ftw
00:40 <edwardk> so when you go through Y from C -> [C^op, Set] you get a bunch of 'set-like stuff' for free.
00:42 <edwardk> Y is a full and faithful functor, that preserves limits (is continuous), but it messes with your colimits. why? well, by going there you now have colimits that are more set-like
00:42 <edwardk> what happens is Y takes C to [C^op, Set] where [C^op, Set] has now has colimits for free, borrowed from Set, assuming C is small, etc.
00:43 <edwardk> Y gives you a 'free cocompletion' of the category C
00:43 <edwardk> (by throwing in colimits in this way)
00:46 <edwardk> from this you get lots of things that have non-trivial structure, the yoneda lemma says Nat(Y a, F) is naturally isomorphic to F a
00:47 <edwardk> (that works for contravariant functors F, but if you do a version of Y where you fix the C^op and go to 'copresheaves' Y^ : C^op -> [C, Set] you still throw in colimits for free, and Nat (Y^ a, F) is naturally isomorphic to F a for the same reasons)
00:48 <edwardk> once you understand kan extensions you can also see the yoneda embedding as a trivial application of taking the right kan extension along the identity functor
00:48 <edwardk> so it pops up over and over
00:50 <spacekitteh> hmm, sweet, thanks
01:24 <benl23> I always liked the poset example:
01:24 <benl23> "a <= b iff for all c we have c <= a implies c <= b"
01:25 <benl23> so..
01:27 <benl23> read "a <= b" as "a comes before b" or "you can get from a to b"
01:29 <benl23> yoneda says that instead of reasoning about the path between a and b directly, you can instead reason about two sets of paths -- the set of paths to a, and the set of paths to b.
01:30 <benl23> .. or something
01:30 <benl23> we need "baby's first category theory"
01:35 <benl23> The poset example always makes sense to me when explained as a diagram with objects and arrows, but it's always a disaster in words.
01:37 <benl23> "you can get from a to b" means the same as "if you can get from all the things to a then you can get from all the things to b"
01:38 <benl23> .. but that's too weak
01:44 <benl23> "you can get from A to B" means the same as "if you can get from C to A then you can get from C to B"