proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.Combinatorics.Lists UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SumOfSignatures UniMath.SubstitutionSystems.BinProductOfSignatures UniMath.SubstitutionSystems.SubstitutionSystems UniMath.SubstitutionSystems.LamSignature UniMath.SubstitutionSystems.Notation UniMath.SubstitutionSystems.BindingSigToMonad UniMath.SubstitutionSystems.LiftingInitial_alt