Proposition equalizer_from_pb_prod_unique : isaprop (∑ (ζ : w --> e), ζ · i = h). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Section EqualizersFromPullbackProducts. End EqualizersFromPullbackProducts. - exact (BinProductsFromPullbacks PB T).