PR #6291: feat(topology/category/profinite): Initial work...

Stream: triage

[Random Issue Bot]

Today I chose PR 6291 for discussion!

feat(topology/category/profinite): Initial work to show that profinite sets are limits of finite discrete sets
Created by @Calle Sönne (@callesonne) on 2021-02-18
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?