{P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {S : CompHausLike P} →
      {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} →
        [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] →
          (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) →
            (a : Function.Fiber ⇑f) → Y.obj (Opposite.op (CompHausLike.LocallyConstant.fiber f a))