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
.