# Commit 2021-05-07 22:54 dbcd4546

View on Github →feat(topology/category/*): Add alternative explicit limit cones for `Top`

, etc. and shows `X : Profinite`

is a limit of finite sets. (#7448)
This PR redefines `Top.limit_cone`

, and defines similar explicit limit cones for `CompHaus`

and `Profinite`

.
Using the definition with the subspace topology makes the proofs that the limit is compact, t2 and/or totally disconnected much easier.
This also expresses any `X : Profinite`

as a limit of its discrete quotients, which are all finite.