Lemma [lcc-000B]

Fix a (Cartesian) distributive category \mathcal {C}. Denote the initial object by 0.

The functor \mathsf {Lens}(\mathcal {C}) \to \mathcal {C} which maps \binom {A}{X} \mapsto X and carries each lens to its forward pass is left adjoint. Its right adjoint is given by X \mapsto \binom {0}{X}. In particular, it preserves coproducts.