Theorem [lcc-000C]

Let X_i \in \mathcal {C} be a collection of objects with coproduct \sum _i X_i. Let A \in \mathcal {C}. Then the family of lenses \binom {A}{X_i} \to \binom {A}{\sum _i X_i} given by the inclusions as the forwards pass, and the projection X_i \times A \to A as the backwards pass, is a coproduct diagram.

This is essentially due to Hedges, in Morphisms of Open Games