Commit 2024-07-01 08:42 ec0fac84

feat(CategoryTheory/SmallObject): the category of transfinite iterations of a functor (#12211) In this PR, we construct the category of transfinite iterations of a functor. We show that there is at most one morphism between two objects in this category. In future PRs, we shall show (by transfinite induction) that there is exactly one (iso)morphism between two objects, and that there is always an object (that is unique up to a unique isomorphism).