∀ {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}))))
  (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X]
  (x y : X.obj (Opposite.op S)) [CompHausLike.HasExplicitFiniteCoproducts P],
  (∀ (a : Function.Fiber ⇑f),
      X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op x =
        X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op y) →
    x = y