∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {Q : CompHausLike P} {Z : Type (max u_1 u_2)} (r : LocallyConstant (↑Q.toTop) Z)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P],
  Function.Injective
      ⇑(CategoryTheory.ConcreteCategory.hom (CompHausLike.ofHom P (TopologicalSpace.Fiber.sigmaIsoHom ⇑r))) ∧
    Function.Surjective
      ⇑(CategoryTheory.ConcreteCategory.hom (CompHausLike.ofHom P (TopologicalSpace.Fiber.sigmaIsoHom ⇑r)))