∀ (X Y : TopCat) (s : CategoryTheory.Limits.BinaryCofan X Y),
  CategoryTheory.CategoryStruct.comp (TopCat.ofHom { toFun := Sum.inl, continuous_toFun := ⋯ })
      (TopCat.ofHom
        { toFun := Sum.elim ⇑(CategoryTheory.ConcreteCategory.hom s.inl) ⇑(CategoryTheory.ConcreteCategory.hom s.inr),
          continuous_toFun := ⋯ }) =
    s.inl