A diagrammatic approach to symmetric lenses

TL;DR

This paper introduces a diagrammatic framework for symmetric lenses using category theory, demonstrating their relationship with spans of asymmetric lenses via an explicit adjoint triple.

Contribution

It presents a novel diagrammatic approach to symmetric lenses and establishes their local adjointness to spans of asymmetric lenses in categorical terms.

Findings

Bicategory of symmetric lenses is locally adjoint to spans of asymmetric lenses.

Constructs an explicit adjoint triple between hom-categories.

Provides a categorical foundation for symmetric lenses.

Abstract

Lenses are a mathematical structure for maintaining consistency between a pair of systems. In their ongoing research program, Johnson and Rosebrugh have sought to unify the treatment of symmetric lenses with spans of asymmetric lenses. This paper presents a diagrammatic approach to symmetric lenses between categories, through representing the propagation operations with Mealy morphisms. The central result of this paper is to demonstrate that the bicategory of symmetric lenses is locally adjoint to the bicategory of spans of asymmetric lenses, through constructing an explicit adjoint triple between the hom-categories.