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. 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.
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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Combinatorics.StandardFiniteSets. Section BinProductFromIso. End BinProductFromIso. Section BinProductsFromProducts. End BinProductsFromProducts. Section ProductsFromBinProducts. End ProductsFromBinProducts.