Characterising asymmetric lenses using internal categories

Asymmetric lenses were originally defined in Computer Science as a solution to the view update problem, and are mathematically well understood as a generalisation of split opfibrations. In this thesis, we utilise internal category theory to unify three kinds of asymmetric lens — set-based, c-lenses, and d-lenses — through the construction of an internal category of view updates produced using the well-known lens laws. We show that this category forms the head of a span of internal functors, which induces a commutative triangle with the Get of a lens. The composition of these commuting triangles is used to characterise the three categories Lens, Clens, and Dlens.