what exactly do you mean by corecursive? (it's guarded, and guarded equations do have unique fixpoints.)
The definition I had in mind is that an arrow g is defined from G by co-recursion "in a single step" if it arises as the unique coalgebra homomorphism from a coalgebra G to the terminal coalgebra. It is defined by co-recusion "in multiple steps" if it is obtained from certain basic morphisms by repeated applications of the above single step, together with basic operations on morphisms. I am not so sure what I mean by "basic"; but I have in mind morphisms and operations that are defined by ordinary equations (as opposed to fixpoint equations) from the structure of the category at hand (such as composition, pairing, the functor "X v Y", etc).
i think such class of corecursive functions would be too narrow: eg, it seems that only a small part of the elements of the final coalgebra (the "rationals") can be captured as corecursive constants, at least as long as your basic operations are finitary. while the class of recursive functions is countable, the class of corecursive functions should not be, if constants are to be included.
What's the exact definition of "guarded" in this context?
in stream and list coalgebra, a fairly obvious semantic condition covers not only the usual syntactical guard conditions, but also the convergence criteria for power series solutions of, say, diff eqns. it's in my CMCS98 paper @article{PavlovicD:GIFC author = "Dusko Pavlovi\'c", title = "Guarded induction on final coalgebras", journal = "E. Notes in Theor. Comp. Sci.", pages = "143--160", year = "1998", volume = "11", url = "http://www.elsevier.nl/locate/entcs", } saying "categorically" which operations are guarded wrt an arbitrary functor is less straightforward... or at least less easy to justify. i worked on this, but never managed to get a really convincing formulation. (a clumsy one is on my web page.) -- dusko