proposition: Proposition is_coend_construction_of_coends_comm : is_cowedge_map is_coend_construction_of_coends_mor.
proof: Proof. intros x. cbn. unfold is_coend_construction_of_coends_mor. unfold construction_of_coends_in. rewrite !assoc'. rewrite CoequalizerCommutes. apply (CoproductInCommutes _ _ _ CoprodF). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Coequalizers