Proposition construction_of_ends_wedge_laws : is_wedge construction_of_ends_wedge_data. Proof. intros x y f. cbn ; unfold construction_of_ends_pr. rewrite !assoc'. pose (maponpaths (λ z, z · ProductPr _ _ _ (x ,, (y ,, f))) (EqualizerEqAr construction_of_ends_ob)) as p. cbn in p. rewrite !assoc' in p. unfold end_left_map, end_right_map in p. refine (_ @ p @ _). - apply maponpaths. refine (!_). exact (ProductPrCommutes _ _ _ ProdM _ _ (x ,, (y ,, f))). - apply maponpaths. exact (ProductPrCommutes _ _ _ ProdM _ _ (x ,, (y ,, 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.Products. Require Import UniMath.CategoryTheory.Limits.Equalizers.