Generalized Lens Categories via functors $\mathcal{C}^{\rm op}\to\mathsf{Cat}$

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 $\mathsf{Lens}_F$ for any category $\mathcal{C}$ and functor $F\colon \mathcal{C}^{\rm op}\to\mathsf{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.