Lemma binproduct_of_isos {C : category} {x1 x2 y1 y2 : C} (p : BinProduct _ x1 x2) (i1 : z_iso x1 y1) (i2 : z_iso x2 y2) : BinProduct _ y1 y2. Proof. use make_BinProduct. - exact p. - exact (BinProductPr1 _ p · i1). - exact (BinProductPr2 _ p · i2). - use (isbinproduct_of_isos p (z_iso_inv i1) (z_iso_inv i2) (identity_z_iso p)) ; rewrite id_left; rewrite assoc'; rewrite z_iso_inv_after_z_iso; now rewrite id_right. 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.