∀ {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)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  CategoryTheory.CategoryStruct.comp
      {
        hom :=
          CategoryTheory.CategoryStruct.id
            (((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp
                    (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj
                c).pt,
        w := ⋯ }
      {
        hom :=
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Functor.id
                    (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj
                c).pt,
        w := ⋯ } =
    CategoryTheory.CategoryStruct.id
      (((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp
            (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj
        c)