Restriction categories I: categories of partial maps

Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par : MCat Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par0 : MCat0 Cat0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories an...

• Type: Journal
• Year: 2002
• Where: TCS
• Authors: J. Robin B. Cockett, Stephen Lack
• Keywords: Associated Idempotent, Partial Maps, Restriction Category, TCS 2002, Theoretical Computer Science