refactor(CategoryTheory/SmallObject): generalization of the definitions

[joelriou]

The ongoing definition of the iteration of a natural transformation ε : 𝟭 C ⟶ F (with F : C ⥤ C) is generalized to "successor structures" (which shall become a mathlibism), i.e. in a category D, this consists of a zeroth object X₀, a successor application succ : D → D and a map toSucc X : X → succ X (which does not have to be natural: it is not always so in some applications). For such a Φ : SuccStruct D, if J is a well-ordered type, we define the J-th iteration of Φ. (In the case J := ℕ, this is the colimit of succ (succ (succ (succ ... X₀))).)

The iteration of a functor is a particular case of this constructor with D := C ⥤ C.

As toSucc does not have to be natural in X, the caveat is that the proofs make extensive use of equalities of objects in C and Arrow C, while my previous construction used comparison isomorphisms. Nevertheless, the proofs look much more clean now. One of the reasons is that in the inductive construction (file Iteration.Nonempty), in the terms of data, we only need to provide a functor, and then all the fields are in Prop. (In the downstream API, we shall obviously use isomorphisms instead of equalities...)

This PR supersedes #19264. The results are used in #20245 in order to get functorial factorizations in the small object argument.

After refactoring my code, I found that this approach had been already been used in 2018 by Reid Barton in his pioneering formalization work in Lean 3 towards the model category structure on topological spaces.

---

• depends on: [Merged by Bors] - feat(CategoryTheory): the class of morphisms given by a family of maps #21354
• depends on: [Merged by Bors] - feat(CategoryTheory): (co)limits indexed by preorders #20335
• depends on: [Merged by Bors] - feat(CategoryTheory/Limits/Shapes/Preorder): principal segments #21055

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): the class of morphisms given by a family of maps #21354
• [Merged by Bors] - feat(CategoryTheory): (co)limits indexed by preorders #20335
• [Merged by Bors] - feat(CategoryTheory/Limits/Shapes/Preorder): principal segments #21055
  By Dependent Issues (🤖). Happy coding!