Definition isBinProduct_is_objectwise {C D : category} {F1 F2 P : [C, D]} {P1 : [C, D] ⟦ P, F1 ⟧} {P2 : [C, D] ⟦ P, F2 ⟧} (Pc_prod : ∏ c: C, isBinProduct D (pr1 F1 c) (pr1 F2 c) (pr1 P c) (pr1 P1 c) (pr1 P2 c)) : BinProducts D -> isBinProduct [C, D] F1 F2 P P1 P2. Proof. intro BP. use make_isBinProduct'. { apply functor_precat_binproduct_cone ; exact BP. } use tpair. - use nat_trafo_z_iso_if_pointwise_z_iso. intro c. set (Pc := make_BinProduct _ _ _ _ _ _ (Pc_prod c)). use make_is_z_isomorphism. + use (BinProductArrow _ Pc). * apply BinProductPr1. * apply BinProductPr2. + split. * etrans. 1: apply (precompWithBinProductArrow D Pc). etrans. 1: apply maponpaths, BinProductPr2Commutes. etrans. 1: apply maponpaths_2, BinProductPr1Commutes. exact (! BinProductArrowId Pc). * etrans. 1: apply (precompWithBinProductArrow D (BP _ _)). etrans. 1: apply maponpaths, (BinProductPr2Commutes D _ _ Pc). etrans. 1: apply maponpaths_2, (BinProductPr1Commutes D _ _ Pc). exact (! BinProductArrowId (BP _ _)). - split. + use nat_trans_eq. { apply homset_property. } intro c. set (Pc := make_BinProduct _ _ _ _ _ _ (Pc_prod c)). apply (BinProductPr1Commutes D _ _ Pc). + use nat_trans_eq. { apply homset_property. } intro c. set (Pc := make_BinProduct _ _ _ _ _ _ (Pc_prod c)). apply (BinProductPr2Commutes D _ _ Pc). 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.