proposition: Lemma z_iso_to_isBinCoproduct {x y z : C} (BP : BinCoproduct x y) (i : z_iso z (BinCoproductObject BP)) : isBinCoproduct C _ _ z ((BinCoproductIn1 BP) · (z_iso_inv_from_z_iso i)) ((BinCoproductIn2 BP) · (z_iso_inv_from_z_iso i)).
proof: Proof. intros w f g. use unique_exists. - exact (i · (BinCoproductArrow BP f g)). - exact (z_iso_to_isBinCoproduct_comm BP i w f g). - abstract (intros y0; apply isapropdirprod; apply C). - abstract (intros y0 T; exact (z_iso_to_isBinCoproduct_unique BP i w f g y0 T)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.ProductCategory