Def CompHaus.limit_cone_is_limit

feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990) …

feat(topology/category/*): Add alternative explicit limit cones for `Top`, etc. and shows `X : Profinite` is a limit of finite sets. (#7448) …