∀ {P : TopCat → Prop} {B X : CompHausLike P} (π : X ⟶ B) {W : CompHausLike P} (e : X ⟶ W),
  (∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X),
      CategoryTheory.CategoryStruct.comp g₁ π = CategoryTheory.CategoryStruct.comp g₂ π →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
    ∀ (a b : ↑X.toTop),
      (CategoryTheory.ConcreteCategory.hom π) a = (CategoryTheory.ConcreteCategory.hom π) b →
        (CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom P { toFun := fun x => a, continuous_toFun := ⋯ })
                e))
            a =
          (CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom P { toFun := fun x => b, continuous_toFun := ⋯ })
                e))
            a