Cocontinuity on over categories

Cocontinuity of a functor between arbitrary sites passes to the induced functor between their over categories. This construction is independent of any geometric realization of the sites.

instance CategoryTheory.Over.post_isCocontinuous {C D : Type u} [Category.{u, u} C] [Category.{u, u} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} (F : Functor C D) [F.IsCocontinuous J K] (X : C) : (post F).IsCocontinuous (J.over X) (K.over (F.obj X))

Cocontinuity passes to the induced functor on over categories.