This short paper addresses a long standing open question about symmetric lenses, with the result succinctly summarised by the paper's title. It has been clear for some years that symmetric lenses of various kinds can be constructed in a systematic way as equivalence classes of spans of asymmetric lenses of corresponding kinds [4]. For example, given a definition of asymmetric delta lens [1], referred to here and elsewhere as a d-lens [3], one can systematically construct a notion of symmetric d-lens [2, 5], and a category whose morphisms are those symmetric d-lenses. Among the d-lenses there are some particularly useful lenses, called c-lenses [7] (and previously known to the mathematical community as split opfibrations) which have an attractive universal property that in many applications corresponds to least change updating. Naturally there has been interest in symmetric c-lenses, which can again be systematically constructed, and which might be expected to have an attractive universal property which could perhaps in applications capture a new notion of least change symmetric lens updating [6]. However, the effects of the universal properties of the component c-lenses of a span of c-lenses occur mainly in the peak of the span, and that corresponds in applications to hidden data. Indeed, it can be shown that every span of c-lenses, viewed as a symmetric lens, is equivalent to a span of d-lenses in which the component d-lenses are not themselves c-lenses. In other words, the behaviour of a symmetric c-lens can always be obtained from a span of lenses which themselves do not have the c-lens universal property. And that raises the until now open question of whether there are in fact any differences at all between symmetric c-lenses and symmetric d-lenses. In this paper we show that a span of c-lenses does have a weak symmetric lens universal property, and that there are spans of d-lenses that do not exhibit this property, establishing that there are symmetric d-lenses which never arise as symmetric c-lenses. In mathematical terms: We look at spans of functors (G; D) with common domain R, and the induced relation (R; G; D) between the codomain categories. We discuss properties of these relations that are satisfied when the legs of the span are opfibrations. More precisely when the left leg G admits a splitting, the relation admits an induced so called a left-right behaviour . Roughly it associates a related morphism on the right to a given morphism on the left. If the splitting is opfibrant then given a factorization on the left, whose composite is related to a morphism on the right, there is a related factorization on the right built from the left-right behaviour and the universal property of the left leg G. We build a counter-example showing that such a factorization on the right cannot always be obtained from a factorization on the left when G is not opfibrant.
Let R and G be categories and R G / G be a functor between them. 2.1
Definition 2.1. Assuming that all our categories are conveniently small, a splitting P for the functor G is a family (Px)x2Ob(R) of functions, indexed by the objects x of R, between unions of homsets with fixed domain: G(G(x); )
Px / R(x; ) The notation R(x; ) denotes the union Sy2Ob(R) R(x; y), and similarly G(G(x); ) = Sz2Ob(G) G(G(x); z). The image Px(f ) of a morphism f with domain G(x) is called the lifting of f at x (by P ) and is required to satisfy G(Px(f )) = f .
Moreover a splitting is required to satisfy: 1. identities of G are lifted to identities of R; 2. if f and g are composable morphisms in G with liftings Px(f ) with codomain y say, and Py(g), then the composite of the liftings, Py(g)Px(f ), is equal to the lifting of the composite, Px(gf ). morphism x
g morphism y t0 / z in R such that g = t0f and G(t0) = t:
/ y in R is said to be opcartesian (with respect to G) if for any other / z such that there exists a morphism G(y) t / G(z) in G with G(g) = tG(f ), there is a unique if
G(x)
G(z) 6 O
t / G(y) then x g f 6 zO / y t0
f G(x) / y in G admits an opcartesian lifting x
The functor G is said to be an opfibration if for every object x in R, each morphism f0
/ y0 (i.e. an opcartesian arrow f 0 such that G(f 0) = f ).
Moreover a splitting P for an opfibration G is a splitting in the sense of Definition 2.1 such that all liftings by P are opcartesian.
The above definitions give precise mathematical representations of d-lenses and c-lenses: d-lenses R G / G are splittings, and c-lenses R G / G are split opfibrations. 2.2
Spans, Relations, and Left-Right Behaviours Given again categories R and G and R G / G a functor between them, let D be another category and R D another functor so that we have the span (R; G; D): / D f G(g) G(f)
R G
D G z $
D Definition 2.4. We define the relation (R; G; D) between G and D associated to the span (G; D) as follows.
Two objects x in G and y in D are defined to be related xRy if and only if there is w in R such that G(w) = x and D(w) = y. We then call w the witness and we sometimes include w in the notation by writing xRwy.
The relation on morphisms is defined similarly.
Of course we have that if f Rqg then the domains and codomains of f and g are related by (R; G; D) with witnesses the domain and codomain of q. Also xRy if and only if idx R idy.
Definition 2.5. Left-right behaviour of (R; G; D):
Given an object x in R we have G(x)RxD(x), and then G(x) and D(x) are called synchronized states.
f Then consider a morphism G(x)
/ y , which we may call a change of state in G, from G(x) to y.
We say that (R; G; D) has a left-right behaviour if for each such choice of x and f , there is a corresponding synchronisation in D, i.e. there is a given morphism (change of state) (f; x) of D with domain D(x) and such that f R (f; x).
One can define a right-left behaviour of a span similarly.
Suppose that G admits a splitting P . Then there exists an induced left-right behaviour, denoted P , defined, for x and f as before, by the lifting of f , x Px(f)/ y0 in R, which yields a common change of state in R.
It then suffices to take the image by D in order to obtain the synchronisation D(x) P (f;x)..=D(Px(f))/ D(y) .
When G and D are both d-lenses, the induced left-right behaviour corresponds to the forward propagation of the corresponding symmetric d-lens, and similarly, the induced right-left behaviour corresponds to the backward propagation. 2.3
Weakly Opcartesian Behaviours We identify now a property of behaviours of (R; G; D) which is not necessarily satisfied in general but which is always satisfied when G is an opfibration.
Definition 2.6. Suppose that (R; G; D) has both a given left-right behaviour and a given right-left behaviour . We define what it means for to be weakly opcartesian with respect to .
Let G(x)RxD(x) be synchronized states and let G(x) forward behaviour to D(x) (f;x)
/ D(y0) .
Consider a change of state D(x) k / z in D, which is carried by the backward behaviour to (k; x): f / y be a change of state which is carried by the Now suppose that there exists a morphism y l / G(z00) such that (k; x) = lf , we then say that is weakly opcartesian with respect to if and only if for each such x, f , k and l, there is an induced l0 in D such that lRl0 and k = l0 (f; x):
G(x) G(x) (k;x)
f (k;x) f 6 G(z00)
/ y G(z00) 6 O / y l
D(x)
k (f;x)
5 z / D(y0): D(x)
k (f;x) 5 zO
l0 / D(y0) Remark 2.7. One may want to think of Definition 2.6 as a particular instance of the property of (R; G; D) which we call left-right-compatible with factorizations: if kRk0 and k factorizes as k = lf in G, then there are l0 and f 0 in D such that lRl0, f Rf 0 and l0f 0 = k0.
Now symmetric lenses are equivalence classes of spans of asymmetric lenses, and it is important to note that the induced left right behaviour is an invariant of the equivalence. Indeed, the reason the equivalence was introduced for symmetric lenses was because differences that aren’t visible in left-right or right-left behaviours are irrelevant for symmetric lenses.
Thus, if a span of lenses induces a left-right behaviour which is weakly opcartesian with respect to its rightleft behaviour , then any equivalent span of lenses also exhibits a left-right behaviour that is weakly opcartesian with respect to its right-left behaviour. In other words, the left-right behaviour being weakly opcartesian with respect to the right-left behaviour is an invariant among representatives of the equivalence class. 3
Lemma 3.1. Given (R; G; D), if G is an opfibration and P is a splitting for it in the sense of Definition 2.3, while D is a functor and S is a splitting for it (so in the sense of Definition 2.1), then the induced left-right behaviour P , is weakly opcartesian with respect to the induced right-left behaviour S .
Proof. Given a synchronization G(x)RxD(x) and a morphism k : D(x) ! z in D, if S (k) factorizes as ts in G, then by the universal property of the opcartesian lifting Px(s) of s, there is an induced t0, as in the diagram below, such that G(t0) = t. Taking the image by D then concludes the proof:
G(x)
S(k;x) s
G(y) 6 O / z t yields x
Sx(k)
Px(s) 7 yO / z0 t0 and thus
D(x) k P (s;x) z = D(y) 5 O
D(t0) / D(z0) Counter-example 3.2. Consider the categories R, G, D, and the functors G, D illustrated in the diagram below. ; u
G(y)
G(f)=G(l) 5 O G(t) G(x)
G(s) / G(z) y x G l f s 5 y
O t / z
D %
D(x)
D(l)
D(f) D(s) : D(u) 5 D(O yD)(t) / D(z)
We observe that the relation (R; G; D) is not left-right-compatible with factorizations since G(l) admits a factorization through G(s) but D(l) does not factorize through D(s). Also G and D may be equipped with splittings, but G cannot be an opfibration since s, the only possible lifting of G(s), is not opcartesian. Under Definition 2.1 there can in this case be only one choice of a splitting for each functor. The splitting of G, P say, gives us an induced left-right behaviour P , and the splitting of D, S say, gives us an induced right-left behaviour S .
The left-right behaviour P is not weakly opcartesian with respect to S . 4
We have just provided a relatively simple counterexample to resolve a longstanding open question. The question was whether the symmetric lenses obtained as equivalence classes of spans of c-lenses, and those obtained as equivalence classes of spans of d-lenses were in fact different.
If the counterexample is so simple, why has it taken so long? It is the theoretical work of this paper that makes the above span of d-lenses into a counterexample. The difficulty is a common problem: Proving that there is no span of c-lenses that is equivalent to the span of d-lenses shown above is, a priori, very difficult. What we have done in this short paper is identify a property of a span of c-lenses that is also present in all equivalent spans of d-lenses. Since that property is not exhibited by the span of d-lenses above, that span cannot be equivalent to any span of c-lenses, thus resolving the question and showing that c-lenses and d-lenses are not coextensive.