Theorem [efr-OSH4]

There exists a (strong) symmetric monoidal functor \mathsf {Optic}(Kl(\Delta )) \to \mathsf {SLens}(Kl(\Delta )^\to ) which

1. Is fully faithful.
2. Preserves the good coproducts.
3. So that the image has all coproducts, and every object of the image is a coproduct of objects in \mathsf {Optic}(Kl(\Delta ))
4. And so that moreover the monoidal structure on the image is distributive