Limits and Colimits in a Category of Lenses

TL;DR

This paper investigates the mathematical structure of the category of small categories and asymmetric delta lenses, establishing the existence of limits, colimits, and other exactness properties relevant to applications.

Contribution

It proves that this category has limits, colimits, imported limits, is extensive, and possesses an image factorisation system, advancing the theoretical understanding of lenses in category theory.

Findings

Existence of limits and colimits in the category of lenses

Presence of imported limits like imported products and pullbacks

The category is extensive and has an image factorisation system

Abstract

Lenses are an important tool in applied category theory. While individual lenses have been widely used in applications, many of the mathematical properties of the corresponding categories of lenses have remained unknown. In this paper, we study the category of small categories and asymmetric delta lenses, and prove that it has several good exactness properties. These properties include the existence of certain limits and colimits, as well as so-called imported limits, such as imported products and imported pullbacks, which have arisen previously in applications. The category is also shown to be extensive, and it has an image factorisation system.