Definition Lenses and charts [efr-0024]

Let \mathcal {A}: \mathcal {C}^\mathrm {op} \to \mathsf {Cat} be an indexed category. A chart is simply a morphism in the Grothendieck construction \int \mathcal {A}. A lens is a morphism in the fiberwise opposite \int \mathcal {A}(-)^\mathrm {op}.