The double category of lenses

A lens is a functor equipped with a suitable choice of lifts, generalising the notion of a split opfibration. Lenses were first introduced in computer science to model bidirectional transformations between systems, and this thesis contributes to an ongoing initiative to understand lenses using category theory. Specifically, we study the mathematical structure of lenses using double categories, and use this to generalise the theory of lenses to new and useful settings. Arguably the most fundamental characterisation of lenses, due to Ahman and Uustalu, is as a compatible functor and cofunctor pair. We introduce the flat double category of cofunctors — consisting of categories, functors, and cofunctors — and examine several of its basic properties. Right-connected double categories were first introduced in the study of algebraic weak factorisation systems, and we establish an explicit construction which completes a double category under this property. The double category of lenses is characterised as the right-connected completion of the double category of cofunctors, and we demonstrate how many properties of lenses are inherited from functors and cofunctors via this construction. In particular, the double category of cofunctors is strongly span representable, and this leads to a diagrammatic calculus for lenses using the right-connected completion. The Grothendieck construction, which yields split opfibrations, is among the most useful notions in category theory, and we introduce a generalised Grothendieck construction for lenses. Given a double category equipped with a functorial choice of companions, its left-connected completion is shown to admit a universal property with respect to lax double functors. The double category of split multi-valued functions is introduced as the left-connected completion of the double category of spans, and we prove that lax double functors into this double category correspond to lenses using the aforementioned universal property. It is well known that functors between categories naturally arise as monad morphisms in the double category of spans, providing the basis for useful generalisations such as internal categories. We introduce the notion of monad retromorphism, and show that in the double category of spans, monad retromorphisms are precisely cofunctors. Using the right-connected completion, lenses between monads are defined, and they are used to develop the theory of lenses and split opfibrations in internal category theory. It is natural to ask if any functor or cofunctor may be equipped with the structure of a lens. We show that lenses arise as both algebras for a monad, and coalgebras for a comonad. It follows that a lens is a functor with additional algebraic structure, and also a cofunctor with additional coalgebraic structure. In particular, the monad for lenses generates an algebraic weak factorisation system, for which every functor factorises through its corresponding free lens. The link between lenses and algebraic weak factorisations systems provides a new setting in which many of the properties of lenses can be understood. While lenses are a generalisation of the notion of split opfibration, the results in this thesis also have implications for split opfibrations themselves, including new characterisations using décalage, strict factorisation systems, and lax double functors. Altogether, the thesis demonstrates that double categories provide a valuable unified framework for the theory of lenses.