Dependent optics [lcc-0003]

Definition Simple Bimorphic Lens [lcc-0001]

Let \mathcal {C} be a Cartesian monoidal category. Then \mathsf {Lens}(\mathcal {C}) is the category whose objects are pairs \binom {X}{A} of objects in \mathcal {C}, where morphisms are defined by \operatorname {\mathrm {Hom}}\left (\binom {X}{A}, \binom {Y}{B}\right ) = \mathcal {C}(X,Y) \times \mathcal {C}(X \times B, A), and where composition is defined by (f^+: X \to Y, f^-: X \times B \to A) ; (g^+: Y \to Z, g^-: Y \times C \to B) \\= (f^+;g^+, (x,c) \mapsto f^-(x,g^-(f^+(x),c))) (The expression of the composite of the backwards passes in terms of elements is easily seen to correspond to a composite of maps between products in a generic Cartesian category)

Polynomial functors as lenses [lcc-0002]

Let \mathcal {C} be a locally Cartesian closed category. Recall the definition of polynomial functor. We will only be interested in the simple case of polynomial endofunctors, which means a polynomial is given simply by a morphism p: A \to X \in \mathcal {C}.

We think of the object p: A \to X as being an X-indexed family of objects, given by the "fibers" p^{-1}(\{x\}) = A_x. Then a transformation of polynomials (p: A \to X) \to (p': B \to Y) consists of a map f^+: X \to Y and a map f^-: B \times _Y X \to A over X. If \mathcal {C} = \mathsf {Set}, this backwards map amounts to a family of maps f^-_x: B_{f(x)} \to A_x

The problem of dependent optics is how to combine both the nondeterminism (or some more general form of effects) of optics with the dependent backwards pass of dependent lenses. The basic issue is that, given a nondeterministic forwards pass p: X \to Y, and an element x \in X, there is no particular element p(x) \in Y so that we can ask for a backwards map B_{p(x)} \to A_x.

The idea, then, is to demand that the forwards stochastic process generate not just an element y by also some residual m \in M which is compatible with the y - that is, there is an indexed family M_{xy}, and we generate a pair y,m \in M_{xy}, and then there is a family of backwards processes q: M_{xy} \otimes B_y \to A_x.

With a little bit of elaboration, this definitions works to produce what you might call coproduct optics or indexed optics - when the indexed object is a coproduct of "trivial" ones, (which is, of course, always the case for sets), we get a suitable definition.

With significantly more elaboration, we get what has been called fibre optics, which is about the widest possible generality for the above idea. It is not entirely clear that this captures everything someone might mean by "dependent optics" - in particular, the cases covered by the definition are forced to be somewhat "Markovesque", in the sense that there has to be a Cartesian subcategory in there.

To elaborate on this, in an ordinary optic, the backwards map M \otimes B \to A doesn't see "the Y part" of the forwards pass X \to M \otimes Y - in a Cartesian or Markov setting, of course, we could just copy the value in Y and pass that along to the residual, so that doesn't matter. But in the general monoidal case, optics might not be able to depend on "which y \in Y happened" (in a sense, this is the whole difficulty of dependent optics). Fibre optics only effectively cover cases where the information which the dependent types depend on can be copied at will.

Fibre Optics [lcc-0005]

Let \mathcal {I} have all finite limits, and equip it with the Cartesian monoidal structure. Let \mathcal {C},\mathcal {M},\mathcal {D} \to \mathcal {I} be bifibrations which have the Beck-Chevalley condition. Suppose \mathcal {M} is a monoidal bifibration in the sense of Framed bicategories and monoidal fibrations, and suppose further that \mathcal {M} acts on \mathcal {C} and \mathcal {D} in a way compatible with the fibrations.

Note that we are only asking for compatibility with the fibration, not with the bifibration - that is, we expect tensors of Cartesian lifts to be again Cartesian, but not that this is the case for coCartesian lifts.

Then the objects of the category of fibre optics, \mathsf {FibOptic}^\mathcal {I}_\mathcal {M}(\mathcal {C},\mathcal {D}), are tuples (I \in \mathcal {I}, X \in \mathcal {C}_I, A \in \mathcal {D}_I) The set of morphisms (I,X,A) \to (J,Y,B) is given by the scary-looking expression \int ^{M \in \mathcal {M}_{I \times J}} \mathcal {C}_\mathcal {I}(X, \pi _J^!(M \cdot \pi _J^*Y)) \times \mathcal {D}_\mathcal {I}(\pi _I^!(M \cdot \pi _J^*B), A)

Apart from the previously mentioned conceptual quibbles, the obvious complexity of the definition is probably the biggest downside to this notion (it's even worse than it looks, since the functors \pi ^*, \pi ^! are only defined up to isomorphism).

The flavor of the intended examples of fibre optics is given by the following construction on Markov categories:

[lcc-0006]

Let \mathcal {C} be a Markov category. We may define a category of "bundles", which we will denote \mathsf {Bun}(\mathcal {C}), as follows: its objects are deterministic maps X \to I \in \mathcal {C}_\mathrm {det}, and its morphisms are squares

where g, but not f, is required to be deterministic.

There is a forgetful functor \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det} which takes X \to I to I. If \mathcal {C} itself is Cartesian, then this is just the codomain opfibration, and this thing will be a bifibration if and only if \mathcal {C} has pullbacks.

In the Markov case, it's not necessarily sufficient that \mathcal {C}_\mathrm {det} has pullbacks. What is required is, given a diagram of this form where all the maps are deterministic:

there is a bijection between (nondeterministic) maps X \to Y making the outer square commute, and maps X \to Y \times _J I making the triangle over I commute. This is true, for example, in \mathsf {FinStoch}, as can be readily verified, and it seems like it "should" be true based on an intuitive model of probability.

If we impose this condition, \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det} becomes not only a bifibration, but a monoidal fibration, and a bifibration with the Beck-Chevalley condition. (The monoidal structure on \mathsf {Bun}(\mathcal {C}) simply being the obvious one). The fibration being monoidal follows from the fact that products of pullback diagrams are pullback diagrams, and the Beck-Chevalley condition holds because it holds for codomain fibrations, and all the morphisms involved in checking it are deterministic

Theorem Fibre Optics for Markov Bundles [lcc-0007]

Let \mathcal {C} be a Markov category, and consider the category of bundles in \mathcal {C}. Suppose \mathcal {C} satisfies the pullback condition for \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det} to be a fibration

Now consider fibre optics applied to the self-action of the fibration \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det}. Let us abbreviate \mathsf {FibOptic}^{\mathcal {C}_\mathrm {det}}_{\mathsf {Bun}(\mathcal {C})}(\mathsf {Bun}(\mathcal {C}),\mathsf {Bun}(\mathcal {C})) by merely \mathsf {FibOptic}(\mathcal {C}). Let us also abbreviate \mathsf {Bun}(\mathcal {C}) = \mathsf {Bun}, and write the fibers as usual as \mathsf {Bun}_I

  • Given two objects (I,X \to I, A \to I), (J, Y \to J, A \to J) of \mathsf {FibOptic}(\mathcal {C}), the set of morphisms can be written as \int ^{M \in \mathsf {Bun}_{I \times J}} \mathsf {Bun}_I(X, M \times _J Y) \times \mathsf {Bun}_I(M \times _J B, A)
  • Given an object (I, Y,B), this object is isomorphic to (Y, Y, B \times _I Y)
  • The set of maps into an object (Y,Y,B) of this form (out of I, X, A) is given by \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X,M) \times \mathsf {Bun}_I(M \times _J B, A).
  • In particular, \mathsf {FibOptic}(\mathcal {C}) is equivalent to the category where objects are deterministic morphisms A \to X \in \mathcal {C}, and the set of morphisms (A \to X) \to (B \to Y) is given by \int ^{M \in \mathsf {Bun}_{X \times Y}} \mathcal {C}_{/X}(X,M) \times \mathcal {C}_{/X}(M \times _Y B, A)
  • The set of maps (X, X, A \times X) \to (Y, Y, B \otimes Y) is in bijection with the set of simple optics \mathsf {Optic}(\mathcal {C})((X,A),(Y,B))

Proof

The first statement is simply rewriting using the fact that the pullback operations f^* are given by actual pullbacks in \mathcal {C}_\mathrm {det}, and so is the local tensor product on each fiber \mathsf {Bun}_I. We also suppress the pushforwards f_!, since they simply change the morphism to the base, which is implicit in this notation anyway. Do note that these pullbacks in \mathcal {C}_\mathrm {det} are not pullbacks in \mathsf {Bun}_I!

For the second statement, by definition the set of maps from an arbitrary test object into (Y,Y,Y \times _J B) is given by \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X, M \times _Y Y) \times \mathsf {Bun}_I(M \times _Y B \times _J Y, A) But clearly M \times _Y Y = M, and similarly M \times _Y B \times _J Y = M \times _J B, so we can write \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X, M) \times \mathsf {Bun}_I(M \times _J B, A) The claim is that this is in bijection with \int ^{M \in \mathsf {Bun}_{I \times J}} \mathsf {Bun}_I(X, M \times _J Y) \times \mathsf {Bun}_I(M \times _J B, A)

We construct a bijection. Given a tuple in the first set M, \phi : X \to M, \psi : M \times _J B \to A, we carry it to M, \phi ;(1_M,p_Y), \psi , by just postcomposing the structural map to Y with Y \to J. The map p_Y is the structural map M \to Y - we form M to M \times _J Y in the obvious way and compose it with \phi . \psi , we can just leave in place.

For the other direction, given a tuple (M, \phi : X \to M \times _J Y, \psi : M \times _J B \to A), we form the tuple (M \times _J Y, \phi , \pi ;\psi ) - here we use the obvious projection \pi : M \times _J Y \times _J B \to M \times _J B.

The functoriality of these constructions makes it easy to verify that they're well-defined. Let's verify they're inverses. In one case, I start with M over J (and I), and obtain M \times _J Y. There is an obvious projection map M\times _J Y \to M, and this witnesses the equivalence of the two optics in this case. In the other case, I start with M over Y, and obtain M \times _J Y again. In this case, it's the diagonal map M \to M \times _J Y which does it.

The third statement is, again, a straightforward rewriting. The fourth statement is just a simple rewriting of the third, plus the observation that, since every object is isomorphic to one of this form, the subcategory on those is equivalent.

For the fifth statement, note that the set of ordinary optics is the set \int ^{M \in \mathcal {C}} \mathcal {C}(X, M \otimes Y) \times \mathcal {C}(M \otimes B, A)\\ \cong \int ^{M \in \mathsf {Bun}_{* \times *}}\mathsf {Bun}_*(X, M \times Y) \times \mathsf {Bun}_*(M \times B, A)\\ \cong \mathsf {FibOptic}(\mathcal {C})((*,X,A),(*,Y,B)) \cong \mathsf {FibOptic}(\mathcal {C})((X,X,X \times A),(Y,Y,Y\times A)), where the last step uses the preceding

References

Reference Framed bicategories and monoidal fibrations [shulman-monfibs]

Abstract

  • January 9, 2009
  • Michael A. Shulman

In some bicategories, the 1-cells are 'morphisms' between the 0cells, such as functors between categories, but in others they are 'objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the 'morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change 'nonalgebraically', using categorical fibrations. The resulting 'framed bicategories' assemble into 2categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones. 

 @article
{shulman-monfibs, title={Framed bicategories and monoidal fibrations}, url={http://arxiv.org/abs/0706.1286}, journal={arXiv:0706.1286 [math]}, author={Shulman, Michael A.}, year={2009}, month={Jan},language={en} }

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.

Definition Simple Optics [lcc-0004]

Let \mathcal {C} be a monoidal category. Then \mathsf {Optic}(\mathcal {C}) is a category where

  • Objects are pairs \binom {A}{X} of objects in \mathcal {C}
  • The set of morphisms is \operatorname {\mathrm {Hom}}\left (\binom {A}{X},\binom {B}{Y}\right ) = \int ^{M \in \mathcal {C}} \mathcal {C}(X, M \otimes Y) \times \mathcal {C}(M \otimes B, A)

Note that many sources, including Categories of optics, write the forwards direction on top, rather than on the bottom as we have done here. Writing the forwards direction on the bottom is in line with the comparison with dependent optics, where the backwards pass is indexed in some sense over the forwards pass.