{P : TopCat → Prop} →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {Q : CompHausLike P} →
      {Z : Type (max u w)} → (r : LocallyConstant (↑Q.toTop) Z) → Function.Fiber ⇑r → CompHausLike P