Proposition is_coend_construction_of_coends_comm : is_cowedge_map is_coend_construction_of_coends_mor. Proof. intros x. cbn. unfold is_coend_construction_of_coends_mor. unfold construction_of_coends_in. rewrite !assoc'. rewrite CoequalizerCommutes. apply (CoproductInCommutes _ _ _ CoprodF). Qed.
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.