{A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {FA : A → A → Type u_2} →
      {CA : A → Type u_3} →
        [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory A FA] →
            [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] →
              (F : CategoryTheory.Functor LightProfiniteᵒᵖ A) →
                [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] →
                  CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A)) →
                    LightCondensed A