∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_6, u_5} C] {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] {F F' : CategoryTheory.Functor C D} (τ : F ⟶ F') (A : Type u_4)
  [inst_2 : CategoryTheory.Category.{u_2, u_4} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K] [inst_4 : F'.IsContinuous J K]
  ⦃X Y : CategoryTheory.Sheaf K A⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F'.sheafPushforwardContinuous A J K).map f)
      { val := CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op τ) Y.val } =
    CategoryTheory.CategoryStruct.comp
      { val := CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op τ) X.val }
      ((F.sheafPushforwardContinuous A J K).map f)