Proposition Equalizer_z_iso_lr_unique {w : C} (h : w --> x₂) : isaprop (∑ φ, φ · ι = h). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.