proposition: Proposition is_end_construction_of_ends_comm : is_wedge_map is_end_construction_of_ends_mor.
proof: Proof. intros x. cbn. unfold is_end_construction_of_ends_mor. unfold construction_of_ends_pr. rewrite !assoc. rewrite EqualizerCommutes. apply (ProductPrCommutes _ _ _ ProdF). 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