Definition hat_exp_functor_list'_optimized_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'_optimized0 xst). Proof. induction xst as [xs t]. set (P := fun xs b' => nat_z_iso (hat_exp_functor_list0 (xs,, t)) b'). refine (foldr1_map_ind _ _ _ P _ _ _ xs). - use tpair. + apply (nat_trans_id (C := sortToC2) (C' := sortToC2)). + intro ; apply (identity_is_z_iso (C := sortToC2)). - intro lt. exact (hat_exp_functor_list'_piece_test (lt,,t)). - intros k xs' m F Hyp. red. use nat_z_iso_comp. 3: { use nat_z_iso_BinProduct_of_functors. 4: exact Hyp. 2: exact (hat_exp_functor_list'_piece_test (m ,, t)). } clear F Hyp. unfold hat_exp_functor_list0, hat_exp_functor_list. unfold exp_functor_list. change (pr1 (cons m (cons k xs'),, t)) with (cons m (cons k xs')). rewrite foldr1_map_cons. 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.