Lemma foldr_app X (fvar : HSET2⟦1,X⟧) (fapp : HSET2⟦X ⊗ X,X⟧) (flam : HSET2⟦X + 1,X⟧) : app_map · foldr_map X fvar fapp flam = # (pr1 (Id * Id)) (foldr_map X fvar fapp flam) · fapp. Proof. assert (F := maponpaths (λ x, CoproductIn _ _ (Coproducts_functor_precat _ _ _ _ _) true · BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · x) (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))). rewrite assoc in F. etrans; [apply F|]. rewrite assoc. etrans. { eapply cancel_postcomposition. rewrite <- assoc. eapply maponpaths, BinCoproductOfArrowsIn2. } rewrite assoc. etrans. { eapply @cancel_postcomposition. eapply @cancel_postcomposition. apply (CoproductOfArrowsIn _ _ (Coproducts_functor_precat _ _ _ _ (λ i, pr1 (Arity_to_Signature BinProductsHSET BinCoproductsHSET TerminalHSET (BindingSigMap LamSig i)) `LC_alg))). } rewrite <- assoc. etrans; [eapply maponpaths, BinCoproductIn2Commutes|]. rewrite <- assoc. etrans; eapply maponpaths. - exact (CoproductInCommutes _ _ _ _ _ _ true). - apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. 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.Chains.All. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Initial. 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.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. 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.LamSignature. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.BindingSigToMonad. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt.