{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          (J : CategoryTheory.GrothendieckTopology C) →
            (K : CategoryTheory.GrothendieckTopology D) →
              (A : Type w) →
                [inst_2 : CategoryTheory.Category.{w', w} A] →
                  [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] →
                    [CategoryTheory.Functor.IsDenseSubsite J K G] → CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf K A