chore(Topology/Category): make finite coproducts in CompHaus univer…

…se polymorphic (#12138)

Mathlib/Topology/Category/CompHaus/Basic.lean

@@ -390,3 +390,15 @@ set_option linter.uppercaseLean3 false in
 #align CompHaus.mono_iff_injective CompHaus.mono_iff_injective
 
 end CompHaus
+
+/--
+Many definitions involving universe inequalities in Mathlib are expressed through use of `max u v`.
+Unfortunately, this leads to unbound universes which cannot be solved for during unification, eg
+`max u v =?= max v ?`.
+The current solution is to wrap `Type max u v` in `TypeMax.{u,v}`
+to expose both universe parameters directly.
+Similarly, for other concrete categories for which we need to refer to the maximum of two universes
+(e.g. any category for which we are constructing limits), we need an analogous abbreviation.
+-/
+@[nolint checkUnivs]
+abbrev CompHausMax.{w, w'} := CompHaus.{max w w'}

Mathlib/Topology/Category/CompHaus/Limits.lean

@@ -24,7 +24,7 @@ So far, we have the following:
 
 namespace CompHaus
 
-universe u
+universe u w
 
 open CategoryTheory Limits
 
@@ -138,7 +138,7 @@ end Pullbacks
 
 section FiniteCoproducts
 
-variable {α : Type} [Finite α] (X : α → CompHaus.{u})
+variable {α : Type w} [Finite α] (X : α → CompHausMax.{u, w})
 
 /--
 The coproduct of a finite family of objects in `CompHaus`, constructed as the disjoint
@@ -158,18 +158,18 @@ To construct a morphism from the explicit finite coproduct, it suffices to
 specify a morphism from each of its factors.
 This is essentially the universal property of the coproduct.
 -/
-def finiteCoproduct.desc {B : CompHaus.{u}} (e : (a : α) → (X a ⟶ B)) :
+def finiteCoproduct.desc {B : CompHausMax.{u, w}} (e : (a : α) → (X a ⟶ B)) :
     finiteCoproduct X ⟶ B where
   toFun := fun ⟨a,x⟩ => e a x
   continuous_toFun := by
     apply continuous_sigma
     intro a; exact (e a).continuous
 
 @[reassoc (attr := simp)]
-lemma finiteCoproduct.ι_desc {B : CompHaus.{u}} (e : (a : α) → (X a ⟶ B)) (a : α) :
+lemma finiteCoproduct.ι_desc {B : CompHausMax.{u, w}} (e : (a : α) → (X a ⟶ B)) (a : α) :
     finiteCoproduct.ι X a ≫ finiteCoproduct.desc X e = e a := rfl
 
-lemma finiteCoproduct.hom_ext {B : CompHaus.{u}} (f g : finiteCoproduct X ⟶ B)
+lemma finiteCoproduct.hom_ext {B : CompHausMax.{u, w}} (f g : finiteCoproduct X ⟶ B)
     (h : ∀ a : α, finiteCoproduct.ι X a ≫ f = finiteCoproduct.ι X a ≫ g) : f = g := by
   ext ⟨a,x⟩
   specialize h a