∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] [inst_3 : CategoryTheory.EssentiallySmall.{u_4, v_1, u_1} C]
  (F : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology (CategoryTheory.SmallModel.{u_4, v_1, u_1} C))
      ((CategoryTheory.equivSmallModel C).inverse.op.comp F)