{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : TopCat} →
      {ι : Type u_1} →
        {B : ι → TopologicalSpace.Opens ↑X} →
          (F : TopCat.Presheaf C X) →
            (F' : TopCat.Sheaf C X) →
              TopologicalSpace.Opens.IsBasis (Set.range B) →
                ((CategoryTheory.inducedFunctor B).op.comp F ⟶ (CategoryTheory.inducedFunctor B).op.comp F'.val) ≃
                  (F ⟶ F'.val)