∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_3} (U : ι → TopologicalSpace.Opens ↑X),
  CategoryTheory.CategoryStruct.comp
      {
        hom :=
          CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op).pt,
        w := ⋯ }
      {
        hom :=
          CategoryTheory.CategoryStruct.id
            ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).symm.functor.obj
                (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U)).pt,
        w := ⋯ } =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)