proposition: Lemma isbinproduct_of_isos {C : category} {x1 x2 y1 y2 py : C} (px : BinProduct _ x1 x2) (i1 : z_iso y1 x1) (i2 : z_iso y2 x2) (i : z_iso py px) (f1 : C ⟦py, y1 ⟧) (f2 : C ⟦py, y2 ⟧) (pf1 : i · BinProductPr1 C px = f1 · i1) (pf2 : i · BinProductPr2 C px = f2 · i2) : isBinProduct _ y1 y2 py f1 f2.
proof: Proof. use make_isBinProduct. intros c g1 g2. use iscontraprop1. - use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use (cancel_z_iso _ _ _ (BinProductArrowsEq _ _ _ px _ (pr1 φ₁ · _) (pr1 φ₂ · _) _ _)). + exact i. + rewrite ! assoc'. rewrite pf1. rewrite ! assoc. apply maponpaths_2. exact (pr12 φ₁ @ ! pr12 φ₂). + rewrite ! assoc'. rewrite pf2. rewrite ! assoc. apply maponpaths_2. exact (pr22 φ₁ @ ! pr22 φ₂). - set (t := pr1 (iso_to_isBinProduct _ px (z_iso_to_iso i) c (g1 · i1) (g2 · i2))). exists (pr1 t). split. + refine (_ @ ! z_iso_inv_on_left _ _ _ _ _ _ (pr12 t)). rewrite assoc'. apply maponpaths. use z_iso_inv_on_left. exact pf1. + refine (_ @ ! z_iso_inv_on_left _ _ _ _ _ _ (pr22 t)). rewrite assoc'. apply maponpaths. use z_iso_inv_on_left. exact pf2. Defined.
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.Monics UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorCategory UniMath.Combinatorics.StandardFiniteSets