Unifying Recursive and Co-recursive Definitions in Sheaf Categories


In this paper we present a theorem for defining fixed-points in categories of sheaves. This result gives a unifying and general account of most techniques used in computer science in order to ensure convergency of circular definitions, such as (but not limited to) well-founded recursion and contractivity in complete ultra metric spaces. This general fixed-point theorem encompasses also a similar set theoretic result presented in previous work, based on the notiotn of ordered family of equivalences, and implemented in the Coq proof assistan

Proceedings of Int. Converence on Foundations of Software Science and Computation Structures (FoSSaCS 04)