Bartosz Milewski's Programming Cafe
In order to define a sheaf, we have to start with coverage. A coverage defines, for every object , a family of covers that satisfy the sub-coverage conditions. Granted, we can express coverage using objects and arrows, but it would be much nicer if we could use the language of functors and natural transformations.
Let’s start with the idea that, categorically, a cover of is a bunch of arrows converging on . Each arrow is a member of the hom-set . Now consider the fact that is a presheaf, , and ask the question: Is a cover a “subfunctor” of ?
A subfunctor of a presheaf is defined as a functor such that, for each object , is a subset of and, for each arrow , the function is a restriction of .
Let’s try to define , such that is non-empty for any object that’s in the cover of , and empty otherwise. As a presheaf, we could represent it as a virtual object with arrows coming from all ‘s.
Now consider an object that is not in the cover, but it has an arrow connecting it to some element of the cover. Functoriality requires the (virtual) composition to exist.
