proposition: Proposition construction_of_ends_wedge_laws : is_wedge construction_of_ends_wedge_data.
proof: 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.
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.Products UniMath.CategoryTheory.Limits.Equalizers