Proposition [efr-2793]

The functor {A \choose X} \mapsto X, \mathsf {Lens}(\mathcal {C}) \to \mathcal {C}, is a fibration. The fiber \mathsf {Lens}(\mathcal {C})_X has the following description:

1. Its objects are the objects of \mathcal {C}.
2. A map A \to B \in \mathsf {Lens}(\mathcal {C})_X is a map X \times B \to A \in \mathcal {C}.
3. The composite of X \times B \to A, X \times C \to B is given by composing the two into X \times X \times C \to A, then using the diagonal.
4. Given f: X \to Y, the pullback functor \mathsf {Lens}(\mathcal {C})_Y \to \mathsf {Lens}(\mathcal {C})_X is given by precomposing by f.