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