Lemma foldr_app X (fvar : sortToSet2⟦Id,X⟧) (fapp : ∏ s t, sortToSet2⟦app_source s t X,X⟧) (flam : ∏ s t, sortToSet2⟦lam_source s t X,X⟧) (s t : sort) : app_map s t · foldr_map X fvar fapp flam = # (pr1 (app_source s t)) (foldr_map X fvar fapp flam) · fapp s t. Proof. etrans; [ apply cancel_postcomposition; unfold app_map; apply assoc |]. rewrite <- assoc. etrans; [apply maponpaths, (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))|]. rewrite assoc. etrans; [eapply cancel_postcomposition; rewrite <- assoc; apply maponpaths, BinCoproductOfArrowsIn2|]. rewrite <- !assoc. etrans; [apply maponpaths, maponpaths, BinCoproductIn2Commutes|]. rewrite assoc. etrans; [apply cancel_postcomposition; use (CoproductOfArrowsIn _ _ (Coproducts_functor_precat _ _ _ _ (λ _, _)))|]. rewrite <- assoc. apply maponpaths. exact (CoproductInCommutes _ _ _ _ _ _ (inl (s,,t))). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. 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.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. 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.Monads.Monads. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. 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.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.SignatureExamples. Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction_alt. Require Import UniMath.SubstitutionSystems.MonadsMultiSorted_alt.