Lemma make_isBinProduct' {C : category} {x y : C} (Pxy : BinProduct _ x y) (z : C) (zx : C⟦z,x⟧) (zy : C⟦z,y⟧) : (∑ i : is_z_isomorphism (BinProductArrow C Pxy zx zy), pr1 i · zx = BinProductPr1 _ Pxy × pr1 i · zy = BinProductPr2 _ Pxy) -> isBinProduct C x y z zx zy. Proof. intros [i [px py]]. use make_isBinProduct. intros c f g. use tpair. - exists (BinProductArrow _ Pxy f g · pr1 i). split. + etrans. 1: apply assoc'. etrans. 1: apply maponpaths, px. apply BinProductPr1Commutes. + etrans. 1: apply assoc'. etrans. 1: apply maponpaths, py. apply BinProductPr2Commutes. - intro co. use total2_paths_f. + apply pathsinv0. use (z_iso_inv_to_right _ _ _ _ (z_iso_inv (_,,i))). apply pathsinv0. use BinProductArrowUnique. * etrans. 1: apply assoc'. etrans. 1: apply maponpaths, BinProductPr1Commutes. exact (pr12 co). * etrans. 1: apply assoc'. etrans. 1: apply maponpaths, BinProductPr2Commutes. exact (pr22 co). + use total2_paths_f ; apply homset_property. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas. Require Import UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts. Require Import UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor. Require Import UniMath.CategoryTheory.Limits.Preservation.