Definition of the category `Arrow C`

Stream: mathlib4

[Robin Carlier]

In file#CategoryTheory/ComposableArrows, @Joël Riou left a TODO suggesting to redefine Arrow C as ComposableArrow C 1 (i.e functors from the free walking arrow to C). Is this still on the table?
I may have a slot this week for investigating this, do you want me to look at it @Joël Riou?

Similarly, Square C is currently an ad hoc structure. Is there an interest of refactoring it as a functor category as well?
Namely, define a WalkingSquare category, and define Square C := WalkingSquare ⥤ C, the two equivalences with Arrow (Arrow C) would then come from equivalences WalkingSquare ≌ Fin 1 × Fin 1 (I guess in fact one of these equivalence could be Equiv.refl).

[Joël Riou]

I think that the best solution is to keep Arrow C (and Square C) as they are, because we have good definitional properties when working in Arrow C (as compared to ComposableArrows C 1). Replacing Arrow with ComposableArrows may lead to issues with automation, and performance (e.g. the equivalence (not in mathlib) between ComposableArrows C 1 and Arrow C is very slow).

[Robin Carlier]

Then, the todo should be removed.

[Joël Riou]

#24572