Lemma iso_to_isBinProduct {x y z : C} (BP : BinProduct C x y) (i : iso z (BinProductObject C BP)) : isBinProduct C _ _ z (i · (BinProductPr1 C BP)) (i · (BinProductPr2 C BP)). Proof. intros w f g. use unique_exists. - exact ((BinProductArrow C BP f g) · (iso_inv_from_iso i)). - abstract (exact (iso_to_isBinProduct_comm BP i w f g)). - abstract (intro; apply isapropdirprod; apply C). - abstract (intros y0 T; exact (iso_to_isBinProduct_unique BP i w f g y0 T)). 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.