∀ {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) {X Y : CompHausLike P} (f : X ⟶ Y),
  CategoryTheory.ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHausLike.toCompHausLike h).map f).hom) = f