Commit 2024-05-08 12:42 feb8ef42

feat(CategoryTheory): more functoriality for Comma categories (#12206) This PR introduces the functor map : Comma L R ⥤ Comma L' R' induced by three functors F₁, F₂, F and two natural transformations F₁ ⋙ L' ⟶ L ⋙ F and R ⋙ F ⟶ F₂ ⋙ R'. Variants for StructuredArrow and CostructuredArrow are also introduced. All the basic functors between Comma categories are special cases of this one, but their definition was not changed: it would break too many defeq.