proposition: Proposition precomp_is_wedge {a : D} (w : wedge) (f : a --> w) : is_wedge (precomp_wedge_data w f).
proof: Proof. intros x y g ; cbn. rewrite !assoc'. rewrite eq_of_wedge. apply idpath. 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