Definition is_coend_construction_of_coends_mor : construction_of_coends_cowedge --> w. Proof. use CoequalizerOut. - use CoproductArrow. exact (λ i, mor_of_cowedge w i). - abstract (use CoproductArrow_eq ; intro f ; unfold coend_left_map, coend_right_map ; rewrite !assoc ; rewrite !(CoproductInCommutes _ _ _ CoprodM) ; rewrite !assoc' ; rewrite !(CoproductInCommutes _ _ _ CoprodF) ; apply eq_of_cowedge). 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.