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