In type theory based logical frameworks, recursive and corecursive definitions are subject to syntactic restrictions that ensure their termination and productivity. These restrictions however greately decrease the expressive power of the language. In this work we propose a general approach for systematically defining fixed points for a broad class of well given recursive definition. This approach unifies the ones based on well-founded order to the ones based on complete metrics and contractive functions, thus allowing for mixed recursive/corecursive definitions. The resulting theory, implemented in the Coq proof assistant, is quite simple and hence it can be used broadly with a small, sustainable overhead on the user.
