∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))),
  CategoryTheory.Presheaf.imageSieve f s =
    {
      arrows := fun V i =>
        ∃ t,
          (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op V))) t =
            (CategoryTheory.ConcreteCategory.hom (G.map i.op)) s,
      downward_closed := ⋯ }