∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u_1 + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u_1 u_2)))
  [inst_3 : CategoryTheory.Limits.PreservesFiniteProducts Y] ⦃X Y_1 : (CompHausLike P)ᵒᵖ⦄ (f : X ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ((CompHausLike.LocallyConstant.functorToPresheaves.obj
            (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u_1 + 1})))).map
        f)
      (match Y_1 with
      | Opposite.op S => CompHausLike.LocallyConstant.counitAppApp S Y) =
    CategoryTheory.CategoryStruct.comp
      (match X with
      | Opposite.op S => CompHausLike.LocallyConstant.counitAppApp S Y)
      (Y.map f)