Proposition [efr-VTPS]

If \mathcal {C} moreover admits pullbacks, there is a fibred functor \mathsf {Lens}(\mathcal {C})^\mathrm {fop} \to \mathcal {C}^\to \to \mathcal {C}, which carries an object {A \choose X} to X \times A\xrightarrow {\pi _X} X, and a morphism f:X \times A \to B to the map X \times A \xrightarrow {\langle \pi _X,F \rangle } X \times B over X. This is fully faithful.