Definition foldr_map X (fvar : HSET2⟦1,X⟧) (fapp : HSET2⟦X ⊗ X,X⟧) (flam : HSET2⟦X + 1,X⟧) : algebra_mor _ LC_alg (make_lambdaAlgebra X fvar fapp flam). Proof. apply (InitialArrow lambdaFunctor_Initial (make_lambdaAlgebra X fvar fapp flam)). 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.