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.
chore(Topology/Category/TopCat): fix universes in continuous_iff_of_isColimit (#28770) The universes were not general enough for certain applications.