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.

Definition 2.1. Assuming that all our categories are conveniently small, a splitting P for the functor G is a family (P x ) x∈Ob(R) of functions, indexed by the objects x of R, between unions of homsets with fixed domain:

The notation R(x, −) denotes the union y∈Ob(R) R(x, y), and similarly G(G(x), −) = z∈Ob(G) G(G(x), z). The image P x (f ) of a morphism f with domain G(x) is called the lifting of f at x (by P ) and is required to satisfy

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 P x (f ) with codomain y say, and P y (g), then the composite of the liftings, P y (g)P x (f ), is equal to the lifting of the composite, P x (gf ).

Definition 2.2. A morphism x f / / y in R is said to be opcartesian (with respect to G) if for any other morphism x g / / z such that there exists a morphism G(y)

G(y)

• The functor G is said to be an opfibration if for every object x in R, each morphism

f / / y in G admits an opcartesian lifting x f / / y (i.e. an opcartesian arrow f such that G(f ) = 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. • 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 xR w y.

• The relation on morphisms is defined similarly.

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 Observations 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)R x D(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 P x (s) of s, there is an induced t , as in the diagram below, such that G(t ) = t. Taking the image by D then concludes the proof: 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 .

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.