∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X),
  Nonempty
    (CategoryTheory.Limits.IsLimit
      (CategoryTheory.Functor.mapCone F.presheaf
        (CategoryTheory.Pairwise.cocone fun j => CategoryTheory.Limits.WalkingPair.casesOn j.down U V).op))