Definition BinProduct_of_functors_distr {C D E : category} (F G : functor C D) (H : functor D E) (Hp : preserves_binproduct H) (BPD : BinProducts D) (BPE : BinProducts E) : nat_z_iso (functor_composite (BinProduct_of_functors BPD F G) H) (BinProduct_of_functors BPE (functor_composite F H) (functor_composite G H)). Proof. set (P := λ c, make_BinProduct _ _ _ _ _ _ (Hp (F c) (G c) _ _ _ (pr2 (BPD (F c) (G c))))). set (i := λ c, iso_between_BinProduct (P c) (BPE (H (F c)) (H (G c)))). use make_nat_z_iso. - use make_nat_trans. + intro c. apply (i c). + intro ; intros. use (z_iso_inv_to_right _ _ _ _ (i x')). etrans. 2: { apply maponpaths_2. apply pathsinv0, (postcompWithBinProductArrow). } cbn. use pathscomp0. * exact (BinProductArrow _ (P x') (#H (pr121 (BPD (F x) (G x)) · # F f)) (#H (pr221 (BPD (F x) (G x)) · # G f))). * use (BinProductArrowUnique _ _ _ (P x')). -- etrans. 1: apply pathsinv0, functor_comp. apply maponpaths, BinProductPr1Commutes. -- etrans. 1: apply pathsinv0, functor_comp. apply maponpaths, BinProductPr2Commutes. * apply pathsinv0. use (BinProductArrowUnique _ _ _ (P x')). -- etrans. 1: apply assoc'. etrans. 1: apply maponpaths, (BinProductPr1Commutes _ _ _ (P x')). etrans. 1: apply BinProductPr1Commutes. apply pathsinv0, functor_comp. -- etrans. 1: apply assoc'. etrans. 1: apply maponpaths, (BinProductPr2Commutes _ _ _ (P x')). etrans. 1: apply BinProductPr2Commutes. apply pathsinv0, functor_comp. - intro c. apply (i c). 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.