Proposition BinCoproduct_z_iso_lr_unique {w : C} (f : x₂ --> w) (g : y₂ --> w) : isaprop (∑ fg, ι₁ · fg = f × ι₂ · fg = g). 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.
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.