proposition: Proposition Equalizer_z_iso_lr_unique {w : C} (h : w --> x₂) : isaprop (∑ φ, φ · ι = h).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply homset_property. } use EqualizerInsEq. refine (_ @ maponpaths (λ z, z · l) (pr2 φ₁ @ !(pr2 φ₂)) @ _). - unfold ι. rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_right. apply idpath. - unfold ι. rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_right. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.BinCoproducts