{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                {S : CategoryTheory.Sheaf J RingCat} →
                  {R : CategoryTheory.Sheaf K RingCat} →
                    [inst_2 : F.IsContinuous J K] →
                      [inst_3 : F.IsContinuous J K] →
                        [inst_4 : G.IsContinuous K J] →
                          [inst_5 : G.IsContinuous K J] →
                            (adj : F ⊣ G) →
                              (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                                (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S) →
                                  CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.val =
                                      CategoryTheory.CategoryStruct.comp ψ.val (G.op.whiskerLeft φ.val) →
                                    CategoryTheory.CategoryStruct.comp φ.val
                                          (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.val)
                                            (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit)
                                              S.val)) =
                                        CategoryTheory.CategoryStruct.id S.val →
                                      (SheafOfModules.pushforward φ ⊣ SheafOfModules.pushforward ψ)