The category of Profinite Types #
We construct the category of profinite topological spaces, often called profinite sets -- perhaps they could be called profinite types in Lean.
Implementation notes #
A profinite type is defined to be a topological space which is compact, Hausdorff and totally disconnected.
- Link to category of projective limits of finite discrete sets.
- finite coproducts
- Clausen/Scholze topology on the category