Commit 2024-04-15 10:00 4932e9d1

View on Github →

chore(Topology/Category): make finite coproducts in CompHaus universe polymorphic (#12138)

Estimated changes

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

modified def CompHaus.finiteCoproduct.desc

modified theorem CompHaus.finiteCoproduct.hom_ext

modified theorem CompHaus.finiteCoproduct.ι_desc