Proposition wedge_map_eq {w₁ w₂ : wedge} {f₁ f₂ : wedge_map w₁ w₂} (p : (f₁ : w₁ --> w₂) = f₂) : f₁ = f₂. Proof. use subtypePath. { intro. use impred. intro. apply homset_property. } exact p. 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.