proposition: Proposition construction_of_coends_cowedge_laws : is_cowedge construction_of_coends_cowedge_data.
proof: 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.
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