Definition is_end_construction_of_ends_mor : w --> construction_of_ends_wedge. Proof. use EqualizerIn. - use ProductArrow. exact (λ i, mor_of_wedge w i). - abstract (use ProductArrow_eq ; intro f ; unfold end_left_map, end_right_map ; rewrite !assoc' ; rewrite !(ProductPrCommutes _ _ _ ProdM) ; rewrite !assoc ; rewrite !(ProductPrCommutes _ _ _ ProdF) ; apply eq_of_wedge). Defined.
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.