Definition hat_exp_functor_list'_test (xst : list (list sort × sort) × sort) (c : propcoproducts_commute_binproducts C BP (λ p, CC p (isasetaprop (pr2 p)))) : nat_z_iso (hat_exp_functor_list0 xst) (hat_exp_functor_list'0 xst). Proof. induction xst as [a t] ; revert a. use list_ind. - use tpair. + apply (nat_trans_id (C := sortToC2) (C' := sortToC2)). + intro ; apply (identity_is_z_iso (C := sortToC2)). - intros x xs IHn. use nat_z_iso_comp. 3: { use nat_z_iso_BinProduct_of_functors. 3: exact IHn. 2: exact (hat_exp_functor_list'_piece_test (x ,, t)). } clear IHn. use (nat_z_iso_comp (post_whisker_nat_z_iso (hat_exp_functor_list'_test_aux x xs) _)). apply BinProduct_of_functors_distr. apply post_comp_functor_preserves_binproduct. + apply BP. + apply (BinProducts_functor_precat _ C BP). + apply hat_functor_preserves_binproducts. exact 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.