new : K1 -> Maybe old : ID -> MaybeThere's an endo-functor Phi on

Phi (F : Set -> Set) = \ X -> X + (F X)^2 + F (Maybe X) : Set -> SetThe 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.