Commit 2025-02-03 19:15 740a8370

View on Github →

feat(CategoryTheory/SmallObject): promote a construction from Over to Arrow (#20260) With this change, in the proof of the small object arguments (#20245), we shall get a functorial factorization instance HasFunctorialFactorization instead of HasFactorization.

Estimated changes