∀ (X : TopCat),
  Function.LeftInverse
    (fun x =>
      ContinuousMap.const
        (↑((CompHausLike.compHausLikeToTop fun x => True).obj
            (Opposite.unop (Opposite.op (CompHaus.of PUnit.{u_1 + 1})))))
        x)
    ⇑(CategoryTheory.ConcreteCategory.hom (CondensedSet.topCatAdjunctionCounit X))