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 notion of ordered family of equivalences, and implemented in the Coq proof assistant.