Commit 2024-06-11 13:06 a3b20f66

refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces (#13319) Changes the definition of LightProfinite to the category of second countable totally disconnected compact Hausdorff spaces. The old LightProfinite is renamed to LightDiagram and we give an equivalence of categories between them. This changes LightProfinite.Basic to match Profinite.Basic more closely. It also contains the equivalence of categories with LightDiagram and an EssentiallySmall instance. The Limits and EffectiveEpi files now match their counterparts for Profinite more closely as well. This PR also adds a new feature: LightProfinite has countable limits and the functor to Profinite creates countable limits.