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
.