Generalized Lens Categories via functors C^ op→Cat
share
Lenses have a rich history and have recently received a great deal of attention from applied category theorists. We generalize the notion of lens by defining a category Lens_F for any category C and functor F: C^ op→Cat, using a variant of the Grothendieck construction. All of the mathematics in this note is straightforward; the purpose is simply to see lenses in a broader context where some closely-related examples, such as ringed spaces and open continuous dynamical systems, can be included.
READ FULL TEXT