Commit 2025-01-06 11:06 14950c53

View on Github →

refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) The current proof that the universe lifting functor for types preserves all colimits is redundant with the work done in CategoryTheory.Limits.Types, in particular with isColimit_iff_bijective_desc, as the result actually follows almost immediately from this last statement. This PR simplifies the proof using isColimit_iff_bijective_desc.

Estimated changes