profinite sets are limits of discrete finite sets

Stream: condensed mathematics

[Calle Sönne]

On the Profinite2 branch I have formalized that profinite sets are limits of finite discrete sets. "Only" ~500 lines. I will start splitting this up into a bunch of smaller PRs soon. Meanwhile, Im looking at Proposition 1.7 in the Condensed mathematics notes as a potential next goal. What was the consensus for what we should do about cardinal bounds? I recall someone (maybe Kevin) saying that we could ignore them by working in a higher universe or something?

[Johan Commelin]

Yup, ignore the set-theoretic issues (for now).

[Kevin Buzzard]

I am right now very much into the "blunder on, ignoring set-theoretic issues" attitude. Occasionally we might have to go all etale cohomology of diamonds section 4 in order to manage some issue, but honestly I think these things are the least of our problems right now.