proposition: Proposition equalizer_from_pb_prod_unique : isaprop (∑ (ζ : w --> e), ζ · i = h).
proof: Proof. use invproofirrelevance. intros ζ₁ ζ₂. use subtypePath. { intro. apply homset_property. } use (MorphismsIntoPullbackEqual (isPullback_Pullback e)). - use (diagonalMap_isMonic P y). rewrite !assoc'. etrans. { apply maponpaths. exact (PullbackSqrCommutes e). } rewrite !assoc. etrans. { apply maponpaths_2. exact (pr2 ζ₁). } rewrite !assoc'. refine (!_). etrans. { apply maponpaths. exact (PullbackSqrCommutes e). } rewrite !assoc. etrans. { apply maponpaths_2. exact (pr2 ζ₂). } apply idpath. - exact (pr2 ζ₁ @ !(pr2 ζ₂)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Pullbacks