In "Re: Algebraically Complete Categories" dybkjaer@euler.ruc.dk (Hans Dybkjaer) writes: Though I do not remember any reference, I do not think that more expressive power in terms of functions N->N is gained by adding other initial algebras , like List. If we restrict our attention to initial algebras for a *polynomial* functor this is true, but in fact if we have an initial algebra for the functor T(X)=1+X+(N=>X) (Coquand-Huet's ordinal notations) we can express the functions $F_{\epsilon_0}$ [1] and even $F_{\Gamma_0}$ [2], where F_ denotes the fast growing hierarchy. These functions are not expressible in G"odel's T. I conjecture that algebraically complete categories are at least as expressive as system F. -- Martin Hofmann References: [1] T. Coquand and C. Paulin-Mohring: "Inductively defined types" in LNCS 389 [2] J. Gallier: "What's so special about Kruskal's theorem and the ordinal $\Gamma_0$" in Annals of pure and applied logic (July 1991) =========================================================================