Commit 2025-08-22 18:35 f21c6a77

View on Github →

chore(Topology/Category/TopCat): fix universes in continuous_iff_of_isColimit (#28770) The universes were not general enough for certain applications.

Estimated changes