Categories of Optics

Understand

Bidirectional data accessors such as lenses, prisms and traversals are all instances of the same general 'optic' construction.

• We give a careful account of this construction and show that it extends to a functor from the category of symmetric monoidal categories to itself.
• We also show that this construction enjoys a universal property: it freely adds counit morphisms to a symmetric monoidal category.
• Missing in the folklore is a general definition of 'lawfulness' that applies directly to any optic category.