Categorical description

On revising this page, I found it to be full of muddle. The endo-functors on Set form a category, in which the morphisms are natural transformations. Among its objects are the constant functor K1 whose value is the ordinal 1, the identity functor ID; and the `Maybe' or (_+1) monad on Set. Among its morphisms are

               new : K1  -> Maybe
               old : ID  -> Maybe

There's an endo-functor Phi on that category which one can write

      
               Phi (F : Set -> Set) 
               = \ X -> X + (F X)^2 + F (Maybe X) 
               : Set -> Set

The abstract syntax of the untyped lambda-calculus can be given as the initial algebra for this composite `higher-order' endo-functor. The initial algebra consists of an object -- in this case the endo-functor L on set -- and a natural transformation into L from (Phi L) given by the constructors Var, App, and Abs.

The category of endo-functors on Set is a pretty scarey place. We can model the syntax in a more hum-drum environment consisting of a subcategory of Set which is closed under Maybe, and contains the necessary maps. However

What is going on here is essentially that we can carry out the whole construction in a universe of `sets' about which we assume nothing but that it is closed under Maybe.