Banach's fixed-point theorem as a base for data-type equations (Q1330915)

The paper develops a theory of data types in categories enriched by CMS (complete metric spaces) analogous to the theory in categories enriched by CPO (complete posets). In this case for a category \({\mathcal K}\) of data types solutions of recursive data-type equations \(X\cong T(X)\), where \(T:{\mathcal K}\to{\mathcal K}\) is a locally continuous endofunctor, can be constructed by iterating \(T\) on the unique arrow \(T:1\to 1\). For CMS enriched categories it is proved that in an analogous manner a solution can be found for data-type equations \(X\cong T(X)\), where \(T\) is a contracting functor, and that this solution is unique.