∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
  (x : (CompHausLike P)ᵒᵖ)
  (a :
    (CompHausLike.LocallyConstant.functorToPresheaves.obj
          (X.obj.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))).obj
      x),
  ((CompHausLike.LocallyConstant.counit P hs).app X).hom.app x a =
    CompHausLike.LocallyConstant.counitAppApp (Opposite.unop x) X.obj a