In this file we construct the functor
Sheaf J A ⥤ Sheaf J B between sheaf categories
obtained by composition with a functor
F : A ⥤ B.
In order for the sheaf condition to be preserved,
F must preserve the correct limits.
Presheaf.IsSheaf.comp says that composition with such an
F indeed preserves the
The functor between sheaf categories is called
sheafCompose J F.
Given a natural transformation
η : F ⟶ G, we obtain a natural transformation
sheafCompose J F ⟶ sheafCompose J G, which we call
sheafCompose_map J η.
The multicospan associated to a cover
S : J.Cover X and a presheaf of the form
P ⋙ F
is isomorphic to the composition of the multicospan associated to
Mapping the multifork associated to a cover
S : J.Cover X and a presheaf
respect to a functor
F is isomorphic (upto a natural isomorphism of the underlying functors)
to the multifork associated to
P ⋙ F.
Composing a sheaf with a functor preserving the appropriate limits yields a functor between sheaf categories.