{I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    [CategoryTheory.IsCofiltered I] →
      {F : CategoryTheory.Functor I FintypeCat} →
        (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
          (X : Type (u + 1)) →
            CategoryTheory.Limits.IsLimit c →
              [∀ (i : I), CategoryTheory.Epi (c.π.app i)] →
                CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone c.op)