For a given behavior type (functor), the carrier of a final coalgebra provides a unique representative for each possible behavior. This property immediately leads to a definition (and proof) principle - called `coiteration' here - for functions from an arbitrary set to this carrier: To define the function's value on a given argument, it suffices to specify a behavior.

Unfortunately it turns out that a large number of functions into a final coalgebra cannot be defined elegantly or not at all using this principle directly. This is due to its limited power for specifying such a behavior, namely declaring a coalgebra structure of the same functor on the domains of the desired function. Extensions of the coiteration schema are wanted.

The corecursion' principle forms such an extension. It is obtained by dualizing the well knownrecursion' - an extension of `iteration' inside the algebraic world. We will try to generalize the ideas behind its construction to arrive at a framework based on pointed endofunctors or monads and appropriate distributive laws.

As one application, the presented setting provides an abstract justification for mutually corecursive definitions. Those have been given (and presented at the ACG colloquium) by Jan Rutten in the context of his coalgebraic treatment of Automata, Power Series, or Control Theory.