Commit 2025-03-17 07:57 02c827e7

refactor(CategoryTheory/Sums): refactor sums of categories (#22976) We refactor the category instance on sums of types so that it is defined even for types living in a different universes. Consequently, we change the order of things related to sums of categories:

• We remove simp instance on Sum.inl_.map and Sum.inr_.map: the inclusions for maps should be considered primitives.
• We make Sum.sum' the first definition about functors out of a sum.
• We add an extensionality (up to isomorphism) theorem for functors out of sums in terms of their precomposition with inl_and inr_.
• We redefine Sum.swap, Sum.associator (as well as its inverse), Functor.sum to use only Sum.sum'.