Lemma foldr_lam X (fvar : HSET2⟦1,X⟧) (fapp : HSET2⟦X ⊗ X,X⟧) (flam : HSET2⟦X + 1,X⟧) : lam_map · foldr_map X fvar fapp flam = # (pr1 (_ o option)) (foldr_map X fvar fapp flam) · flam. Proof. assert (F := maponpaths (λ x, CoproductIn _ _ (Coproducts_functor_precat _ _ _ _ _) false · BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · x) (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))). rewrite assoc in F. unfold lam_map, τ, tau2_from_alg. rewrite assoc. etrans; [apply F|]. rewrite assoc. etrans. { eapply cancel_postcomposition. rewrite <- assoc. eapply maponpaths, BinCoproductOfArrowsIn2. } rewrite assoc. etrans. { eapply @cancel_postcomposition, @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 _ _ _ _ _ _ false). - 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.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.LamSignature. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.SubstitutionSystems.BindingSigToMonad. Require Import UniMath.SubstitutionSystems.LiftingInitial_alt.