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.
Cite
@article{arxiv.1704.02230,
title = {Coherence for lenses and open games},
author = {Jules Hedges},
journal= {arXiv preprint arXiv:1704.02230},
year = {2017}
}