proposition: Proposition BinCoproduct_z_iso_lr_unique {w : C} (f : x₂ --> w) (g : y₂ --> w) : isaprop (∑ fg, ι₁ · fg = f × ι₂ · fg = g).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use BinCoproductArrowsEq. - refine (_ @ maponpaths (λ z, l · z) (pr12 φ₁ @ !(pr12 φ₂)) @ _). + unfold ι₁. rewrite !assoc. rewrite z_iso_inv_after_z_iso. rewrite id_left. apply idpath. + unfold ι₁. rewrite !assoc. rewrite z_iso_inv_after_z_iso. rewrite id_left. apply idpath. - refine (_ @ maponpaths (λ z, r · z) (pr22 φ₁ @ !(pr22 φ₂)) @ _). + unfold ι₂. rewrite !assoc. rewrite z_iso_inv_after_z_iso. rewrite id_left. apply idpath. + unfold ι₂. rewrite !assoc. rewrite z_iso_inv_after_z_iso. rewrite id_left. 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