Internal lenses

Bryce Clarke – 21 November 2018

Lenses were originally defined in Computer Science as a solution to the view update problem. In 2011 Diskin defined a variant, called a d-lens, which may be understood as a split opfibration without its universal property. In this talk, we define internal lenses and show they induce a commuting triangle of internal categories and functors. These triangles compose to yield the category Lens, and we demonstrate both Diskin's d-lenses and split opfibrations as special cases.