Local categories: a new framework for partiality
Marcello Lanfranchi, Jean-Simon Pacaud Lemay
TL;DR
The paper unifies four categorical approaches to partiality—restriction categories (partiality on morphisms), local categories (partiality on objects), partial categories (operational with restriction/contraction), and inclusion categories (inclusions)—via a web of 2-equivalences. It develops the core constructions L and R to translate between restriction and local frameworks, and extends these correspondences to Cartesian, split, inverse, and join variants. A bounded version of each theory is shown to be 2-equivalent to the others, providing four interchangeable descriptions of partiality and enabling transfer of concepts across frameworks. The results also connect to the Ehresmann-Schein-Nambooripad theory for inverse structures through inverse local/inclusion categories, offering a broad, unified view of partiality with potential applications in logic, semantics, and computation.
Abstract
Restriction categories provide a categorical framework for partiality. In this paper, we introduce three new categorical theories for partiality: local categories, partial categories, and inclusion categories. The objects of a local category are partially accessible resources, and morphisms are processes between these resources. In a partial category, partiality is addressed via two operators, restriction and contraction, which control the domain of definition of a morphism. Finally, an inclusion category is a category equipped with a family of monics which axiomatize the inclusions between sets. The main result of this paper shows that restriction categories are $2$-equivalent to local categories, that partial categories are $2$-equivalent to inclusion categories, and that both restriction/local categories are $2$-equivalent to bounded partial/inclusion categories. Our result offers four equivalent ways to describe partiality: on morphisms, via restriction categories; on objects, with local categories; operationally, with partial categories; and via inclusions, with inclusion categories. We also translate several key concepts from restriction category theory to the local category context, which allows us to show that various special kinds of restriction categories, such as inverse categories, are $2$-equivalent to their analogous kind of local categories. In particular, the equivalence between inverse (restriction) categories and inverse local categories is a generalization of the celebrated Ehresmann-Schein-Nambooripad theorem for inverse semigroups.