Definition nat_z_iso_BinProduct_of_functors {C D : category} (F1 F2 G1 G2 : functor C D) (BP : BinProducts D) : nat_z_iso F1 G1 -> nat_z_iso F2 G2 -> nat_z_iso (BinProduct_of_functors BP F1 F2) (BinProduct_of_functors BP G1 G2). Proof. intros α1 α2. use make_nat_z_iso. - use make_nat_trans. + intro c. use BinProductOfArrows. * apply α1. * apply α2. + intros x y f. etrans. 1: apply postcompWithBinProductArrow. etrans. 2: apply pathsinv0, postcompWithBinProductArrow. etrans. 1: apply maponpaths_2, assoc'. etrans. 1: apply maponpaths_2, maponpaths, (pr21 α1). etrans. 2: apply maponpaths_2, assoc. apply maponpaths. etrans. 1: apply assoc'. etrans. 1: apply maponpaths, (pr21 α2). apply assoc. - intro. apply BinProductOfArrows_is_z_iso. + apply (pr2 α1). + apply (pr2 α2). 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.