Proposition construction_of_coends_cowedge_laws : is_cowedge construction_of_coends_cowedge_data. Proof. intros x y f. cbn ; unfold construction_of_coends_in. rewrite !assoc. pose (maponpaths (λ z, CoproductIn _ _ _ (y ,, x ,, f) · z) (CoequalizerEqAr construction_of_coends_ob)). cbn in p. rewrite !assoc in p. unfold coend_left_map, coend_right_map in p. refine (_ @ p @ _). - apply maponpaths_2. refine (!_). exact (CoproductInCommutes _ _ _ CoprodM _ _ (y ,, (x ,, f))). - apply maponpaths_2. exact (CoproductInCommutes _ _ _ CoprodM _ _ (y ,, (x ,, f))). 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.