universe issue in def of condensed

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

I note that we currently have

Condensed.{u, u_1, u_2} (C : Type u_1) [inst✝ : CategoryTheory.Category C] : Type (max (max (max (u + 1) u_1) u) u_2)

That's a lot of universes. Is it true that when we talk about "condensed X" we always have X a large category? The universe of the solution isn't even optimally expressed, there's a u and u+1 in there.

[Scott Morrison]

If you don't specalize to large categories, you should at least change the order of universe parameters. u_1 if inferred from C, but u_2 is presumably the morphism level and so should come first.

[Adam Topaz]

fixed in #5574