Commit 2024-04-13 10:09 4d302c53

adding Functor.sum', dual to Functor.prod'. (#12073) We add Functor.sum' a variant of Functor.sum. This situation is dual to docs#CategoryTheory.Functor.prod'. We also add inl_sum' and inr_sum' which prove that the sum functor F.sum' G precomposed with the left (resp. right) inclusion functor is isomorphic to F (resp. G).