Coproducts in the category of lenses [coprods-lens-blogpost]

Introduction

The category of bimorphic lenses and its many generalizations has been widely studied and utilized in applied category theory. We will not give a review of the literature here, but see e.g. Riley's paper on "optics" (one of the many generalizations) Reference [riley-optics], which includes a decent overview.

Dispensing with a point of notation, we will denote objects of the category of lenses \binom {A}{X}, and morphisms \varphi : \binom {A}{X} \to \binom {B}{Y} as (\varphi ^+: X \to Y,\varphi ^- : X \times B \to A). Note that we write the *forwards* pass on the bottom of the tuple, breaking with the convention used by Riley and many others.

The category \mathsf {Lens}= \mathsf {Lens}(\mathsf {Set}) of lenses embeds into the category of polynomial functors \mathsf {Poly} and natural transformations as the full subcategory of functors of the form X \times (-)^A. Since \mathsf {Poly} admits all coproducts, and these are computed pointwise, one immediate consequence is that we have the coproducts \binom {A}{X} + \binom {A}{Y} = \binom {A}{X + Y} in \mathsf {Lens}. These seem to have been studied first by Hedges (Reference [hedges-morphisms-open-games]). (For a reference on \mathsf {Poly}, including this inclusion, see eg Spivak Reference [spivak-poly-abundant]. \mathsf {Poly} is another branch on the tree of generalizations of \mathsf {Lens}, studied extensively by Spivak and others).

Given the above, one might expect these to be all the coproducts of \mathsf {Lens} (up to isomorphism) - they are certainly the only ones preserved by this inclusion11 There is a quibble here, since \binom {A}{0} \cong \binom {B}{0} for any sets A,B, these being the initial objects of \mathsf {Lens}. This is of course the natural "nullary" version of the binary formula, but it also means that \binom {A}{0}+\binom {B}{X} = \binom {B}{X}, and that this coproduct is preserved by the inclusion into \mathsf {Poly}, even if A \not \cong B. . But this turns out not to be the case.

Let's begin with a worked example of the "exotic" coproducts. Note that I simply denote by n \in \mathbb {N} the set \{1, \dots n\} with n elements. In particular 0 is the empty set.

Example

In \mathsf {Lens}, \binom {0}{1} + \binom {1}{1} = \binom {0}{2}, with the coproduct inclusions having as their forwards pass the two distinct maps 1 \to 2, and the backwards passes in both cases being trivial.

To see this is a coproduct, consider the natural transformation

\mathsf {Lens}\left (\binom {0}{2},\binom {A}{X}\right ) \to \mathsf {Lens}\left (\binom {0}{1},\binom {A}{X}\right ) \times \mathsf {Lens}\left (\binom {1}{1},\binom {A}{X}\right )

In the case where A is nonempty, this is simply the map 0 \to 0, because there are no maps 2 \times A \to 0, and also no maps 1 \times A \to 0. Clearly 0 \to 0 is a bijection. On the other hand if A is empty, all the backwards passes are trivial, so we're just left with the map \mathsf {Set}(2,A) \to \mathsf {Set}(1,A) \times \mathsf {Set}(1,A), which is clearly a bijection. Hence this is a natural isomorphism, so we have a coproduct.

To see why this is not preserved by the inclusion \mathsf {Lens}\hookrightarrow \mathsf {Poly}, consider the polynomial y \mapsto y + 1 (this is the actual coproduct of the polynomials corresponding to these lenses). The inclusion maps from y = 1 \times y^1 and 1 = 1 \times y^0 into this polynomial should induce a map from 2 = 2 \times y^0, but of course there's no way to map into the y (unless we map the entire thing into the 1 component, but this clearly won't pull back to the inclusion map of y when we compose with the map y \to 2). The problem is that, where in the lens/monomial case, to have any maps at all the backwards set must be 0, making the whole backwards pass trivial, in the polynomial case we can have the backwards set be empty only when it's forced to be.

The coproducts in \mathsf {Lens}

Having seen the above, we may begin to lose hope of understanding the coproducts in \mathsf {Lens} at all. Fortunately the situation is not completely chaotic - in some sense, the preceding example is the *only* problem - all the coproducts in \mathsf {Lens} are either of the form \binom {A}{\coprod _i X_i} (up to isomorphism), or they are of the same form as the example.

Theorem

In \mathsf {Lens}= \mathsf {Lens}(\mathsf {Set}), a tuple of lenses \{\binom {A_i}{X_i} \overset {\varphi _i}{\to } \binom {B}{Y}\} is a coproduct diagram if and only if the forwards passes \{X_i \to Y\} form a coproduct diagram in \mathsf {Set}, and one of these conditions hold:

  1. For all i, and for all x \in X_i, the function \varphi _i(x, -): B \to A_i is a bijection.
  2. For at least one i, A_i is empty and X_i is nonempty. (The existence of any lens \binom {A_i}{X_i} \to \binom {B}{Y} then implies that B must be empty as well)

The first class of coproducts are the "good" ones - these are preserved by the functor from lenses to polynomial functors, and seem to capture the correct notion of "branching" for bidirectional systems. The other class, the "exotic" coproducts, are more mysterious.

We will begin the proof of this theorem with some preliminaries about lenses in a general (Cartesian) distributive category. While we can't obtain the preceding theorem in this generality (for reasons that will become clear later), it may be useful to know what can be said here.

Let us fix a (Cartesian) distributive category \mathcal {C} - that is, \mathcal {C} has finite products and coproducts, and the universal map \coprod _i A \times X_i \to A \times (\coprod _i X_i) is always an isomorphism. I will denote the initial object by 0.

Proposition

The functor \mathsf {Lens}(\mathcal {C}) \to \mathcal {C} which carries \binom {A}{X} to X and a lens (\varphi ^+, \varphi ^-) to its foward pass \varphi ^+ admits a right adjoint, given by X \mapsto \binom {0}{X}.

Proof

We simply have to verify \mathsf {Lens}(\mathcal {C})(\binom {A}{X},\binom {0}{Y}) = \mathcal {C}(X,Y). But this is trivial - the forwards pass of such a lens is clearly an element of the right-hand side, so it suffices to prove that there is always a unique choice of backwards pass. But the backwards pass is a map 0 \times X \to A, and by distributivity 0 \times X is initial. This concludes the proof.

Because left adjoints preserve (in particular) coproducts, we obtain the following:

Corollary

For a tuple \{\binom {A_i}{X_i} \overset {\varphi _i}{\to } \binom {B}{Y}\} to be a coproduct diagram, the forwards passes X_i \to Y must form a coproduct diagram in \mathcal {C}.

The following result, characterizing the "good" coproducts, was already essentially proven by Hedges in Reference [hedges-morphisms-open-games]22 Hedges states it only for \mathcal {C} = \mathsf {Set}, but his proof goes through unaltered for our case. He also only constructs a particular family of coproduct diagrams, but the ones considered here are just his composed with isomorphisms in \mathsf {Lens}, so there is really nothing serious going on , but I'll state it here and sketch a proof for completeness.

Proposition

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

Proof

\mathsf {Lens}(\mathcal {C})(\binom {A}{\coprod _i X_i},\binom {B}{Y}) = \mathcal {C}(\coprod _i X_i, B) \times \mathcal {C}((\coprod _i X_i) \times B, a) \cong \prod _i \left (\mathcal {C}(X_i, B) \times \mathcal {C}(X_i \times B, a)\right ),

using the universal property of coproducts and the distributivity. This is clearly the set of tuples of lenses \binom {A}{X_i} \to \binom {B}{Y}, and moreover precomposition with the inclusion maps clearly picks out the elements of the tuple, verifying the universal property of the coproduct.

Proposition

Let a tuple \{\binom {A_i}{X_i} \overset {\varphi _i}{\to } \binom {B}{\coprod _i X_i}\} be given, such that each \varphi _i^+: X_i \to \coprod _j X_j is the coproduct inclusion.

Given some object C \in \mathcal {C}, each \varphi _i^-: X_i \times B \to A_i determines a map (\varphi _i^-)^*: \mathcal {C}(X_i \times C, B) \to \mathcal {C}(X_i \times C, A_i) , given by (\varphi _i^-)^*\psi (x,c) = \varphi _i^-(x,\psi (x,c)). The tuple (\varphi _i) is a coproduct diagram if and only if, for all C, one of these conditions hold (not necessarily the same one for each C):

1. Each (\varphi _i^-)^* is a bijection.

2. For some i, the set \mathcal {C}(X_i \times C, A_i) is empty.

Proof

Note that each of the lenses \varphi _i factors as \binom {A_i}{X_i} \to \binom {B}{X_i} \to \binom {B}{\coprod X_i} = \coprod _i \binom {B}{X_i}, where the first map is (1_{X_i},\varphi _i^-), and the second map is the coproduct inclusion.

Hence the natural transformation

\alpha : \mathsf {Lens}(\mathcal {C})\left (\binom {B}{\coprod _i X_i},\binom {C}{Z}\right ) \to \prod _i \mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right )

factors as

\mathsf {Lens}(\mathcal {C})\left (\binom {B}{\coprod _i X_i},\binom {C}{Z}\right ) \cong \prod _i\mathsf {Lens}(\mathcal {C})\left (\binom {B}{X_i},\binom {C}{Z}\right ) \to \prod _i\mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right )

where the second map is the parallel product of the precomposition morphisms - \circ (1_{X_i},\varphi _i^-) for each i.

The tuple is a coproduct diagram if and only if this composite is a bijection, which is true if and only if this second map is a bijection.

A product of functions in \mathsf {Set} is a bijection if and only if each component map is a bijection, or one of the product sets in the target is empty (in which case the corresponding set in the domain must be empty as well for a map to exist, and so both products are empty).

We can rewrite the sets involved here as

\mathsf {Lens}(\mathcal {C})\left (\binom {B}{X_i},\binom {C}{Z}\right ) = \mathsf {Set}(X_i,Z) \times \mathsf {Set}(X_i \times C, B),

and

\mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right ) = \mathsf {Set}(X_i,Z) \times \mathsf {Set}(X_i \times C, A_i).

This is simply the definition of \mathsf {Lens}

Under this expansion the map - \circ (1_{X_i},\varphi _i^-) carries a lens (\psi ^+, \psi ^-) to (\psi ^+, (\varphi _i^-)^*\psi ^-). So - \circ (1_{X_i},\varphi _i^-)i is a bijection if and only if we have \mathsf {Set}(X_i,Z) empty or (\varphi _i^-)^* a bijection (or both).

Now, clearly if condition 1. holds, we've just seen that each - \circ (1_{X_i},\varphi _i^-) becomes a bijection, and so our map \alpha is a bijection. If condition 2. holds, then \mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right ) is empty, and so we again have a (trivial) bijection.

So if at least one of the conditions hold for each C, \alpha is always a bijection, and so we have a coproduct.

On the other hand, suppose there is some C so that neither condition holds. Take Z = \coprod _i X_i. Then none of the mapping sets \mathsf {Set}(X_i, Z = \coprod _i X_i) are empty, so the only way for - \circ (1_{X_i},\varphi _i^-) to be a bijection is for (\varphi _i^-)^* to be a bijection, but by hypothesis this fails for at least one i. By assumption none of the sets \mathsf {Set}(X_i \times C, A_i) are empty, and none of the sets \mathsf {Set}(X_i, Z) are empty either, so the product is not empty - hence the map \alpha is not a bijection in this case.

We can now return to the main theorem. The following argument is somewhat clunky and ad hoc. The main point is that we can characterize the cases where \mathsf {Set}(U,V) is empty, namely only when V is empty and U is not. In a general category, this can be much more complicated, and there does not seem to be any completely general method. This means we don't know which possible C we need to deal with when understanding when the backwards pass is a bijection, which makes it seemingly impossible to give a general classification of the coproducts by this method.

(The second point is that it's easy to understand when the maps between hom-spaces are bijections in \mathsf {Set} - we have a somewhat clunky argument but it's pretty straightforward and it can probably be done in a more conceptual way, if one took the time to find it).

We can replace Y with the coproduct \coprod _i X_i, and each forwards pass \varphi _i^+ with the inclusion, without loss of generality (if we are not in this situation up to isomorphism, we don't have a coproduct by the above)

Proof Proof of the theorem

It's clear that the first condition of the theorem implies that \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is a bijection always, and so we have a coproduct. As for the second condition, suppose X_i is nonempty and A_i is empty. Then for nonempty C, the set \mathsf {Set}(X_i \times C, A_i) is clearly empty, fulfilling the second condition of the lemma, whereas for empty C, the map \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is a map between two singletons (since X_i \times C is empty), and hence a bijection.

This proves that if one of the two conditions hold, we have a coproduct. To see the other direction, suppose neither condition holds. If the second condition doesn't hold, then there is always a map X_i \to A_i, and hence the set \mathsf {Set}(X_i \times C, A_i) is never empty, so according to the lemma, it suffices to show that for some i and some C, the map (\varphi _i^-)^*: \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is not a bijection.

Since the first condition doesn't hold, let j, x' \in X_j be such that the map \varphi ^-_j(x',-): B \to A_j is not a bijection. Suppose first it's not surjective and let a' be something not in the image.

Take C = *. Then the constant function - \mapsto a' : X_j \times * \to A_j is clearly not in the image of (\varphi _j^-)^*, since that would require, for some \psi , \varphi _j^-(x,\psi (x,*)) = a' for all x, and in particular for x = x', but that's a contradiction.

On the other hand suppose it's not injective, and that \varphi _j^-(x',b_0) = \varphi _j^-(x',b_1) for some b_0,b_1 \in B. Now take C = B and consider a function \psi : X_j \times B \to B, defined by \psi (x',b_0) = b_1, and \psi (x,b) = b for all other pairs (x,b). Now \varphi _j^-(x',\psi (x',b_0)) = \varphi _j^-(x',b_1) = \varphi _j^-(x',b_0). And for all other x or b, clearly \varphi _j^-(x,\psi (x,b)) = \varphi _j^-(x,b). Hence (\varphi _j^-)^*\psi = (\varphi _j^-)*(\pi _B: X_j \times B \to B) (\pi _B being the projection). But \psi \neq \pi _B, so (\varphi _j^-)^* is not injective in this case. This concludes the proof.

The forwards part of this proof almost works for any distributive category \mathcal {C} with a *strict* initial object (meaning the only maps X \to 0 are isomorphisms, i.e X has to be another initial object). The trouble is that X_i \times C can be initial even when neither X_i nor C is, meaning even when A_i is initial and X_i isn't, the nonemptyness of \mathsf {Set}(X_i \times C, A_i) does not imply that C is initial, meaning that we don't automatically get that all the (\varphi _i^-)^* maps are bijections. A simple example of this is something like \mathcal {C} = \mathsf {Set}^k for some natural number k > 1. Then as long as we have C^{(n)} empty *or* X_i^{(n)} empty for each n = 1 \dots k, their product is empty.

A more general class of example with the same flavor is \mathcal {C} = Sh(X) the category of sheaves on a topological space. Then again as long as the supports of C and X_i are disjoint, their product is empty.

It may be possible to develop a generalization of the theorem, or at least of the forwards part of the theorem, using considerations like these to control the sets of morphisms.

References

Reference Morphisms of Open Games [hedges-morphisms-open-games]

  • April 4, 2021
  • Jules Hedges 
@article{hedges-morphisms-open-games,
  title = {Morphisms of open games},
  url = {http://arxiv.org/abs/1711.07059},
  abstract = {We define a notion of morphisms between open games, exploiting a surprising connection between lenses in computer science and compositional game theory. This extends the more intuitively obvious definition of globular morphisms as mappings between strategy profiles that preserve best responses, and hence in particular preserve Nash equilibria. We construct a symmetric monoidal double category in which the horizontal 1-cells are open games, vertical 1-morphisms are lenses, and 2cells are morphisms of open games. States (morphisms out of the monoidal unit) in the vertical category give a flexible solution concept that includes both Nash and subgame perfect equilibria. Products in the vertical category give an external choice operator that is reminiscent of products in game semantics, and is useful in practical examples. We illustrate the above two features with a simple worked example from microeconomics, the market entry game.},
  journaltitle = {{arXiv}:1711.07059 [cs, math]},
  author = {Hedges, Jules},
  urldate = {2021-04-04},
  date = {2017-11-23},
  langid = {english},
  eprinttype = {arxiv},
  eprint = {1711.07059},
  keywords = {Mathematics - Category Theory, Computer Science - Computer Science and Game Theory},
}

Reference Poly: An abundant categorical setting for mode-dependent dynamics [spivak-poly-abundant]

Abstract

  • June 11, 2020
  • David I. Spivak

Dynamical systems---by which we mean machines that take time-varying input, change their state, and produce output---can be wired together to form more complex systems. Previous work has shown how to allow collections of machines to reconfigure their wiring diagram dynamically, based on their collective state. This notion was called “mode dependence”, and while the framework was compositional (forming an operad of re-wiring diagrams and algebra of mode-dependent dynamical systems on it), the formulation itself was more “creative” than it was natural. In this paper we show that the theory of mode-dependent dynamical systems can be more naturally recast within the category Poly of polynomial functors. This category is almost superlatively abundant in its structure: for example, it has emph{four} interacting monoidal structures $(+,times,otimes,circ)$, two of which ($times,otimes$) are monoidal closed, and the comonoids for $circ$ are precisely categories in the usual sense. We discuss how the various structures in Poly show up in the theory of dynamical systems. We also show that the usual coalgebraic formalism for dynamical systems takes place within Poly. Indeed one can see coalgebras as special dynamical systems---ones that do not record their history---formally analogous to contractible groupoids as special categories. 

 @article
{spivak-poly-abundant, title={Poly: An abundant categorical setting for mode-dependent dynamics}, url={http://arxiv.org/abs/2005.01894}, DOI={10.48550/arXiv.2005.01894}, abstractNote={Dynamical systems---by which we mean machines that take time-varying input, change their state, and produce output---can be wired together to form more complex systems. Previous work has shown how to allow collections of machines to reconfigure their wiring diagram dynamically, based on their collective state. This notion was called “mode dependence”, and while the framework was compositional (forming an operad of re-wiring diagrams and algebra of mode-dependent dynamical systems on it), the formulation itself was more “creative” than it was natural. In this paper we show that the theory of mode-dependent dynamical systems can be more naturally recast within the category Poly of polynomial functors. This category is almost superlatively abundant in its structure: for example, it has emph{four} interacting monoidal structures $(+,times,otimes,circ)$, two of which ($times,otimes$) are monoidal closed, and the comonoids for $circ$ are precisely categories in the usual sense. We discuss how the various structures in Poly show up in the theory of dynamical systems. We also show that the usual coalgebraic formalism for dynamical systems takes place within Poly. Indeed one can see coalgebras as special dynamical systems---ones that do not record their history---formally analogous to contractible groupoids as special categories.}, number={arXiv:2005.01894}, publisher={arXiv}, author={Spivak, David I.}, year={2020}, month={Jun} }

Reference Categories of optics [riley-optics]

  • 2018
  • Mitchell Riley 
 @article
{riley-optics, title={Categories of optics}, journal={arXiv preprint arXiv:1809.00738}, author={Riley, Mitchell}, year={2018} }

Backlinks

Wild coproducts in the category of simple lenses [lcc-0008]

This note contains material previously posted on my blog, here

The category of simple (bimorphic) lenses (let's just say over \mathsf {Set}, for now) has a monoidal structure, given by \binom {A}{X} \otimes \binom {B}{Y} = \binom {A \times B}{X \times Y}, which is neither Cartesian nor coCartesian. It also has Cartesian products, given by \binom {A}{X} \times \binom {B}{Y} = \binom {A + B}{X \times Y}. However, it does not in general have coproducts.

In the category of containers/dependent set lenses/polynomials, which is an extension of \mathsf {Lens}(\mathsf {Set}), coproducts do exist. If we think of an element of this category as a base set X and an indexed family of fiber sets A_x, x \in X, then the coproduct just takes the disjoint union of the bases and combines the two indexed families.

The polynomials in the image of \mathsf {Lens}(\mathsf {Set}) are those where the family is constant - B_x = B for all x - and so the problem with \mathsf {Lens}(\mathsf {Set}) when it comes to coproducts is that, if A \ncong B, computing the coproduct of \binom {A}{X} and \binom {B}{Y} in polynomials takes us out of lenses. And indeed in the case A = B, these coproducts do exist in \mathsf {Lens}(\mathsf {Set}) and are given by \binom {A}{X + Y}.

This defect is part of what motivated the development of Dependent optics.

For a while, it was thought that coproducts of this form were the only coproducts in \mathsf {Lens}(\mathsf {Set}), and that therefore the category of dependent lenses could be constructed as the universal completion under coproducts of \mathsf {Lens}(\mathsf {Set}) preserving the existing coproducts. This would then provide a universal property for a category of dependent optics as well.

Unfortunately, this is not true. \mathsf {Lens}(\mathsf {Set}) has the following "wild" coproduct as well:

Example [lcc-0009]

In \mathsf {Lens}{\mathsf {Set}} \binom {0}{1} + \binom {1}{1} = \binom {0}{2}. To see this, let \binom {A}{X} be a test object, and consider \operatorname {\mathrm {Hom}}(\binom {0}{1}, \binom {A}{X}) \times \operatorname {\mathrm {Hom}}(\binom {1}{1},\binom {A}{X}). If A is empty, the backwards pass is trivial in both cases, and so this just amounts to choosing two points of X. If A is nonempty, it is impossible to define the backwards pass in the first map (or the forwards pass, if X is also empty), and so this product is empty. On the other hand, \operatorname {\mathrm {Hom}}(\binom {0}{2}, \binom {A}{X}) is exactly the same - if A is empty, it is X^2, and if A is nonempty, it is the empty set. Hence this is a coproduct.

We have the following theorem characterizing all the coproducts in \mathsf {Lens}(\mathsf {Set})

Theorem [lcc-000A]

In \mathsf {Lens} = \mathsf {Lens}(\mathsf {Set}), a tuple of lenses \binom {A_i}{X_i} \overset {\phi _i}{\to } \binom {B}{Y} is a coproduct diagram if and only if the forwards passes X_i \to Y form a coproduct diagram in \mathsf {Set} and one of these conditions hold:

  1. For all i, and for each x \in X_i, the function \phi ^-(x, -): B \to A_i is a bijection
  2. For at least one i, A_i = \emptyset and X_i is nonempty. (In this case the existence of any lens \phi _i: \binom {A_i}{X_i} \to \binom {B}{Y} implies that B is also empty)

Proof

We divide the proofs into a few lemmata, which may be of some independent interest. It is unfortunate that this result only holds for \mathsf {Lens}(\mathsf {Set}), and not for \mathsf {Lens}(\mathcal {C}) with \mathcal {C} a general Cartesian category. The statement as given is not true in general, but hopefully the proof will give an idea of how these things work in a general Cartesian category.

Lemma [lcc-000B]

Fix a (Cartesian) distributive category \mathcal {C}. Denote the initial object by 0.

The functor \mathsf {Lens}(\mathcal {C}) \to \mathcal {C} which maps \binom {A}{X} \mapsto X and carries each lens to its forward pass is left adjoint. Its right adjoint is given by X \mapsto \binom {0}{X}. In particular, it preserves coproducts.

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

Lemma [lcc-000E]

Let \binom {A_i}{X_i} \overset {\phi }{\to } \binom {B}{\coprod _j X_j} be a tuple of lenses, where the forwards pass \phi ^+_i in each case is given by the coproduct inclusion X_i \to \coprod _j X_j.

Given an object C \in \mathcal {C}, each backwards pass \phi _i^+: X_i \times B \to A determines a map (\phi _i^-)^*: \mathcal {C}(X_i \times C, B) \to \mathcal {C}(X_i \times C, A), given on elements by (\phi _i^-)^*(\psi )(x,c) = \phi ^-_i(x,\psi (x,c)). The tuple (\phi _i) is a coproduct diagram if, for all C, one of these conditions hold (note the order of the quantifiers, here!)

  1. Each (\phi ^-_i)^* is a bijection
  2. For some i, the set \mathcal {C}(X_i \times C, A_i) is empty.

Proof

Note that \binom {B}{\sum _i X_i} \cong \sum _i \binom {B}{X_i}, and each of the \phi _i factors as \binom {A_i}{X_i} \to \binom {B}{X_i} \to \sum _i \binom {B}{X_i}.

Hence if \binom {C}{Z} is a test object, the natural transformation \mathsf {Lens}(\mathcal {C})(\binom {B}{\sum _i X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) is isomorphically the morphism \prod _i \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) given by the product of the precomposition maps.

The tuple is a coproduct diagram if and only if this is a bijection. A product of maps in \mathsf {Set} is a bijection if and only if either each individual map is a bijection, or one of the sets in the codomain product is empty (in which case both products must be empty).

We can rewrite the individual sets as follows: \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, B) \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, A_i) by definition of \mathsf {Lens}. The precomposition maps then carry (\psi ^+, \psi ^-) to (\psi ^+, (\phi _i^-)^*\psi ^-).

So clearly, if condition 1 holds---if each (\phi _i^-)^* is a bijection---each of these maps is a bijection, as desired. If condition 2 holds, both products are empty. This establishes the forwards direction: if, for each C, one of the conditions hold, the natural transformation is a bijection, and so we have a coproduct.

On the other hand, let C be so that neither condition holds. Take Z = \sum _i X_i.

By assumption all of the sets \mathcal {C}(X_i \times C, A_i) are nonempty, and so are the sets \mathcal {C}(X_i, Z). Hence neither product is empty, so each map must be a bijection. But by assumption there is some i where this is not the case.

Now we are ready to prove the theorem.

Without loss of generality, we can assume we are in the situation of Lemma [lcc-000E], where the forwards passes are given by coproduct inclusions.

Now we will use the two following observations:

  1. If C is empty, the map (\phi _i^-)^*: \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is always a bijection, since it is a map between two singleton sets. If C is nonempty, it is a bijection only if the lens (1_{X_i},\phi ^-_i): \binom {A_i}{X_i} \to \binom {B}{X_i} is an isomorphism, i.e only if each of the maps \phi ^-_i(x,-): B \to A_i are bijections
  2. The set \mathcal {C}(X_i \times C, A_i) is empty if and only if X_i, C are nonempty, and A_i is empty

Verifying the first statement is routine but somewhat tiresome. The second statement is trivial.

Hence, if (\phi _i) form a coproduct diagram, by taking C any nonempty set, we find that condition 1. of Lemma [lcc-000E] implies condition 1. of this theorem. And condition 2., implies there is some i with X_i nonempty and A_i empty, so in either case, we have what we wanted. Conversely, if either of the conditions of this theorem hold, they imply the corresponding condition of Lemma [lcc-000E], and so we have the desired equivalence.