Definition coend_left_map : CoprodM --> CoprodF. Proof. use CoproductArrow. intro f ; cbn. refine (#F (_ ,, _) · CoproductIn _ _ _ (pr1 f)). - exact (identity _). - exact (pr22 f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers.