∀ {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z),
  CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h') (F.stalkSpecializes h) = F.stalkSpecializes ⋯