Title: Coherence for lenses and open games,
Abstract: Categories of polymorphic lenses in computer science, and of open games in
compositional game theory, have a curious structure that is reminiscent of
compact closed categories, but differs in some crucial ways. Specifically they
have a family of morphisms that behave like the counits of a compact closed
category, but have no corresponding units; and they have a `partial' duality
that behaves like transposition in a compact closed category when it is
defined. We axiomatise this structure, which we refer to as a `teleological
category'. We precisely define a diagrammatic language suitable for these
categories, and prove a coherence theorem for them. This underpins the use of
diagrammatic reasoning in compositional game theory, which has previously been
used only informally.