Recently lens-like de nitions of multidirectional transformations have appeared [2], encompassing both a \propagation" form (in the style of [5]) and a \wide span" form (in the style of [6]). These \multiary lenses" raise a number of new challenges that are addressed in this paper. First, in common with classical symmetric lenses, they need to be studied modulo equivalence relations that factor out di erences in hidden data and declare two lenses to be equivalent if their observable behaviours correspond. Then, modulo those equivalence relations the precise relationship between the propagation style lenses and the wide span lenses needs to be established. All of this is carried through here. But more signi cantly, the compositions of multiary lenses proposed to date have su ered various limitations: well-behaved amendment lenses don't necessarily compose to give well-behaved amendment lenses; technical conditions on model spaces can interfere with composition; junction conditions needed to be introduced because certain kinds of compositions of multiary lenses might not always be de ned; and in any case, composition of multiary lenses comes with unusual challenges and can't be expected to form a category structure since when there are more than two data sources there are not even single notions of domain or codomain for multiary lenses. In this paper we introduce a class of asymmetric amendment lenses called spg-lenses (stable putget lenses) which is more general than well-behaved amendment lenses, but is closed under composition, and we show how to use spg-lenses to capture, via wide spans, a wide class of mutidirectional transformations which compose well and form a well-known and long-standing structure, a multicategory | a multicategory of multiary lenses.
Bidirectional tranformations have always been intended to, in concert, support multiple interacting systems,
and a great many example such systems have been in operation for many years. Indeed, it's likely that the
majority of systems using bidirectional transformations involve more than two systems, and in some cases they
were operating before the term \bidirectional transformation" was coined. Now, nally, with the recent Dagstuhl
meeting on Multidirectional Transformations and Synchronisations, and the paper of Diskin et al on Multiple
Model Synchronisation with Multiary Delta Lenses [
This paper is a contribution to that work. Originally it began as an analysis of some examples of wide spans of d-lenses and how they might interact, but some of those results have been saved for a future paper as the theoretical nature of those wide spans and their \compositions", let us call them linkages for now, took on more importance, and since the introduction by Diskin and his colleagues of amendment lenses promised substantial generalisations, but also some serious complications.
Among the most serious complications, Diskin and his colleagues had needed to introduce so-called junction
conditions because apparently reasonable linkages among their multiary delta lenses might not lead to
wellde ned multiary delta-lenses. But on an even more basic level, the question of what linkages one might expect
to have between multiary lenses, and how they might be organised and managed algebraically, needs to be
considered. Traditional binary lenses, whether asymmetric or symmetric, form the arrows of categories [
The paper begins by analysing a simpli cation and generalisation of amendment lenses, called here aa-lenses, and exploring their composability. We identify a new and promising class of aa-lenses which we call spg-lenses because they are in Diskin et al's terminology Stable and satisfy the PutGet condition. These spg-lenses are closed under composition, but are a very general class of amendment lenses, being more general than well-behaved amendment lenses (which is not to imply that they are ill-behaved!), and are thus a promising building block for more complex structures including multiary lenses.
We then study n-wide spans of spg-lenses, beginning with n = 2, to see how they might support a \composition" analogous to symmetric lens composition. As Diskin et al discovered, (wide) spans of amendment lenses don't necessarily compose. We organise the linkages among wide spans by requiring that each wide span have an identi ed leg, herein assumed without loss of generality to be the leftmost leg, which is a closed aa-lens, and show that linkages of the left leg of one wide span with any non-left leg of another wide span do indeed result in a new \composite" wide-span of aa-lenses, again with closed leftmost leg. We should remark that this identi ed closed leftmost leg is not a loss of generality | one can consider any n-wide span of aa-lenses that might arise in any application, and if it doesn't have any closed leg one can simply adjoin a lens, possibly even an identity lens, to use as the closed leftmost leg. If it helps, the reader may like to think of the identi ed leftmost leg as a lens which gives access to the head of the span so that compositions can be carried out.
We should also emphasise that the closed leftmost leg does not have any implications for how the n-wide span operates as a multiary lens | any one of the legs, including, but not only, the leftmost leg, might su er a modi cation of state, and as in bidirectional transformations, or multidirectional transformations when n > 2, the other legs will have their state updated to restore synchronisation.
But what of the algebraic structure that these multiary lenses and their linkages should exhibit? As noted
above, it can't be merely a category since there is no consistent notion of domain and codomain. Instead, as the
title of the paper suggests, these multiary lenses, consisting of wide spans of spg-lenses with closed left leg, form
a well-known and long standing algebraic structure known as a multicategory [
The paper is organised as follows. In Section 2 we set out the basic de nitions required based on work of
Diskin et al [
We begin with some background. The following de nitions are close to those of Diskin et al [
Denote the set of objects of a category A by jAj. In the context of n-ary symmetric lenses i will always be an integer between 1 and n.
De nition 1 An n-ary multimodel space (n 2 ) M = (A; R; ) consists of the following data: (i) An n-tuple of categories A = (A1; : : : ; An) (ii) A set R whose elements are called (consistent) corrs (iii) A function : R / jA1j : : : jAnj called the boundary function.
A consistent multimodel is a pair (R; (A1; : : : ; An)) (with Ai an object of Ai) such that (R) = (A1; : : : ; An) = ( 1R; : : : ; nR). For consistent multimodels (R; (Ai)); (R0; (A0i)). a multimodel update is an n-tuple of morphisms (u1; : : : ; un) : (A1; : : : ; An) / (A01; : : : ; A0n).
Notice that a corr and the boundary function determine a consistent multimodel, so we can just dispense with the (Ai) in the notation, as is implicit below.
De nition 2 An n-ary symmetric lens L = (M; p) is an n-ary multi model space, M, and an n-tuple p = (p1; : : : ; pn) of operations as follows. For a consistent multimodel (R; (A1; : : : ; An)) and morphism ui : Ai / A0i, pi returns: (i) A consistent multimodel (R00; (A010; : : : ; A0n0)) with R00 denoted piR(ui) (ii) An amendment uia : A0i / A0i0 denoted piRi (ui) (iii) A multimodel update (u01; : : : ; u0n) : (A1; : : : ; An) / (A010; : : : ; A0n0) such that u0i = uiaui and, when j 6= i, the j-th component u0j is denoted piRj (ui).
Call an update ui R-closed when piRi (ui) = idA0i . The lens L is called closed if all updates are R-closed for all R.
For consistency with earlier work we might have written the operations pi(R; ui), and pii(R; ui); pij (R; ui)
and that would avoid superscripts which complicate the reading and sometimes clash with primes. But for ease
of comparison with [
De nition 3 An n-ary symmetric lens L = (M; p) is called well-behaved if it satis es the following conditions: (Stability): For all j, piRj (idAi ) = idAj and piR(idAi ) = R (Re ect2): For j 6= i, piRj (uiaui) = piRj (ui) (Re ect3): uiaui is R-closed
Notice that stability for a well-behaved n-ary symmetric lens means a trivial update propagates trivially. The
Re ect conditions mean respectively that an amendment \completes" its update, and that a completed update
needs no amendment. There is no (Re ect1) because in [
(Invert): For j 6= i, piRj (pjRi(piRj (ui))) = piRj (ui)
The n-ary symmetric lenses, and their basic properties, have been introduced because they correspond well to
some workers' intuitions of multiary transformations. Diskin et al [
The following is derived from Diskin et al's asymmetric lenses with amendments but we exclude the so-called compatibility relations K, and call the resulting simpli cation (and generalisation) aa-lenses. De nition 5 An aa-lens L = (A; B; g; p), often abbreviated to just (g; p) when there is little risk of confusion, consists of categories A and B sometimes called the base and view model spaces respectively, with g : A / B a functor called the Get and p = fpA j A 2 Ag a family of operations as follows: to every view update v : g(A) / B0, pA returns a pair (pbA(v) : A / A00; paA(v) : B0 / B00) such that B00 = g(A00). A view update v : g(A) / B0 is called closed if paA(v) = idB0 . If all view updates are closed we call L a closed aa-lens.
The requirements for a well-behaved aa-lens based on [
De nition 6 An aa-lens is L = (A; B; g; p) is called well-behaved if the following hold for A 2 A and v : g(A) / B0: (Stability): pbA(idg(A)) = idA (Re ect0): B0 = g(X) for some X 2 A implies paA(v) = idB0 (Re ect2): pbA(paA(v)v) = pbA(v) (PutGet): paA(v)v = g(pbA(v))
There is no (Re ect1) property since we are following [
As noted in [
An aa-lens de nes a well behaved, invertible 2-ary symmetric lens whose base updates (the updates in A) are
closed. A closed aa-lens which also satis es a PutPut law is exactly the same thing as an asymmetric delta lens
[
A further condition considered by Diskin [personal communication] is (Re ect0*): If v = g(w) for w an arrow with domain A of A then paA(v) = idB0 . 3
We now consider the composition of aa-lenses.
De nition 7 Let L = (A; B; g; p) and L0 = (B; C; h; q) be aa-lenses. Their composite aa-lens is L0L = (A; C; k; r) where k = hg and the composite Put r is de ned as follows. If w : hg(A) / C0, then rbA(w) = pbA(qbg(A)(w)) and raA(w) = h(paA(qbg(A)(w))) qag(A)(w). See the diagram, where v = paA(qbg(A)(w)):
A g(A) hg(A) pbA(qbg(A)(w))
/ A" qg(A)(w) b / B0
v / B" w / C0qag(A)(w/ )C00 h(v) / C000
The lens L = (A; A; idA; pA) where for u : A / A0, we have (pA)bA(u) = u and (pA)aA(u) = idA0 is the identity for the just de ned composition, and the reader can easily verify that the composition is associative. Thus there is a category whose objects are model spaces and whose morphisms are aa-lenses. It generalises the category of (asymmetric) delta lenses.
Proof. The proofs all involve routine veri cations which we omit.
Note however that if L and L0 satisfy Re ect2, it does not apparently follow that L0L does so. Indeed it seems that even if L and L0 are well-behaved then the composite need not satisfy Re ect2. This means that we do not have a category of well-behaved aa-lenses. Instead a convenient category of aa-lenses has as arrows those aa-lenses which satisfy Stability and PutGet.
If spg-lenses make up the most convenient category of aa-lenses, we are going to be interested in symmetric
spg-lenses | those that arise as equivalence classes of spans of spg-lenses. However, it seems that spans of
arbitrary spg-lenses can't be assumed to compose in the usual way, analogous to spans of d-lenses [
Proof. Consider two spans of spg-lenses with heads S and T shown in the diagram and suppose that the lenses (g; p) and (g0; p0) are both closed. Let U be the pullback in cat of h and g0, with k and m the pullback projections.
(g;ps)sss X ysss
S(ysKks;srs)sss U KKKK(mKK;Ks% )
(hK;KqK)KKK% Y ysss(sgss0;sp0T) KKKK(hKK0qK0%)Z We de ne r and s making the pairs (k; r) and (m; s) spg-lenses. Since U is a pullback in cat, we may suppose without loss of generality that its objects are compatible pairs of objects, one each from S and T, and that its arrows are compatible pairs of arrows, one from each of S and T. In each case \compatible" means that applying h to an object or arrow from S, and g0 to an object or arrow from T, results in the same object or arrow of Y.
The Put r takes an object (S; T ) of U and an arrow : k(S; T ) = S / S0 of S and returns rb(S;T )( ) an arrow of U with domain (S; T ) and an amendment ra(S;T )( ) in S with domain S0. Let rb(S;T )( ) = ( ; p0bT (h( ))) and let ra(S;T )( ) = ids0 . To see that (k; r) is an spg-lens, note rst that it is stable since h is a functor and (g0; p0) is stable, and secondly it satis es PutGet by construction. Furthermore, (k; r) is closed by construction (all amendments are identities).
The de nition of s is a little longer because its amendments are not as trivial. The Put s takes an object (S; T ) of U and an arrow : m(S; T ) = T / T 0 and returns s(bS;T )( ) an arrow of U with domain (S; T ) and an amendment s(aS;T )( ) in T with domain T 0. Let qaS (g0( )) = b say and de ne s(aS;T )( ) = p0bT 0 (b) = ~b say. Finally, let s(S;T )( ) = (qbS (g0( )); ~b ). To see that (m; s) is an spg-lens, it is stable by an argument parallel b to the argument for (k; r) noting that amendments for identities are identities, and again it satis es PutGet by construction.
The resulting span with head U from X to Z is again a span of spg-lenses and its left leg is closed since spg-lenses compose and closed spg-lenses compose to give closed spg-lenses.
We remind the reader that compositions like this are analogous to span composition in a category with pullbacks. However, U need not be the pullback in the category whose arrows are aa-lenses. It is a pullback in cat, and we have just given canonical constructions on the projection functors to make them into aa-lenses. To emphasise this distinction, while conserving the analogy, we sometimes refer to U along with (k; r) and (m; s) as a \pullback" | the inverted commas remind us that it is not in fact a pullback in spg-lens.
In the following sections we will be studying a generalisation of a span of lenses. An n-wide span of lenses is a tuple L = (A; (Bi; gi; pi)i n) of lenses with a common domain A. We will mostly be considering aa-lenses.
We next consider two constructions relating n-ary symmetric lenses to n-wide spans of aa-lenses.
For the rst construction, we begin with a stable n-ary symmetric lens M = (M; p) with multimodel space M = ((Ai); R; ) and propagation operations pi. The domain and codomain of an arrow u are denoted d0(u) and d1(u) respectively.
We construct an n-wide span LM of spg-lenses (LM )i : S / Ai (similar to a construction in [
(vi)(ui) = (viui) in S(R; R00). The identities are tuples of identities. It is immediate that S is a category.
Next de ne the spg-lens (LM )i = (gi; pi) where gi : S /Ai on objects is i, and on arrows is gi((uj )j n) = ui. The Put for (LM )i has as amendment piR;a( : gi(R) / Ai) = piRi ( ), and has as base Put an arrow of S: (piR;b( : gi(R)) (piR;b( : gi(R)) / Ai)j / Ai)i = = piRj ( ) for j 6= i
R pii ( ) which is indeed an arrow of S from R to R00 = piR( ).
Proof. The gi are evidently functorial. We need to show that pi satisfy the de nition of spg-lens. This follows immediately from the stability of the n-ary symmetric lens M and the construction.
For the construction in the other direction, we begin with an n-wide span L of spg-lenses. Let Li = (gi; pi) where gi : S / Ai.
Construct the n-ary symmetric lens ML = (M; p) with consistent corrs R = jSj, with i(S) = gi(S) and with pi de ned as follows for : gi(S) / A0i: piS ( ) = d1(piS;b( )) piSi( ) = piS;a( ) piSj ( ) = gj (piS;b( )) for j 6= i.
Proof. We have de ned all of the required parts of the pi and stability follows from the stability of the component spg-lenses. 5
We are going to need equivalence relations for n-ary symmetric lenses and for n-wide spans of spg-lenses. The idea is that equivalent lenses/spans have the same update behaviour.
De nition 13 Let L1 = (M; p) and L2 = (N; q) be n-ary symmetric lenses with M = (A; R1; 1) and N = (A; R2; 2) (so they have the same base categories but di erent corrs).
We say L1 n L2 if and only if there is a relation from R1 to R2 with the following properties: 1. is compatible with the i's, i.e. R1 R2 implies iR1 = iR2 n is generated by relations , as in the de nition, which are surjective
3. If R1 R2 (so iR1 = iR2) and ui : Ai / A0i is an arrow of Ai then piR1 (ui) qiR2 (ui) and piRj1 (ui) = qiRj2 (ui) for j = 1; : : : ; n (so they have the same Put behaviour and amendments).
Notice that
is an equivalence relation. Condition 3 implies that the codomains for all piRj1 (R1) are the same as the codomains for all qiRj2 (R2):
Proof. To see that tabulating : n is generated by such surjections, consider L1 n L2 by
and construct the span R1 o
Q / R2 Notice that each leg of the span is a surjection because of totality of a lens with corrs Q equivalent to both L1 and L2 by those surjections. in both directions. It is easy to construct De nition 15 Let L1 = (S1; (Ai; gi; pi)i n) and L2 = (S2; (Ai; gi0; p0i)i n) be n-wide spans of spg-lenses with the same feet. We say L1 is E-related to L2 if and only if there is a functor : S1 / S2 such that (E1) gi0 = gi; i = 1; : : : ; n (E2) is surjective on objects, and (E3) If S1 = S2, then for ui : gi(S1) = gi0(S2) / A0i, we have p0i;a(ui) = pi;a(ui) and p0iS;b2 (ui) = piS;1b(ui):
Condition (E3) says rst that the amendments, which are arrows of Ai, agree, and secondly that the Put behaviours correspond by .
De nition 16 Let relatedness.
spg be the equivalence relation on n-wide spans of spg-lenses which is generated by EProposition 17 With the notation of the constructions above, for n-ary symmetric lenses M = (M; p) and N = (N; q) with M n N , we have LM spg LN .
Proof. Suppose M = (A; R1; 1) and N = (A; R2; 2) are equivalent by relating R1 and R2. Without loss of generality, by Lemma 14, it su ces to assume is a surjective function. Suppose the wide spans constructed from M and N have heads S1 and S2 respectively. We will de ne a functor : S1 / S2 with as its object function. On an arrow of S1, that is a tuple u = (ui) of arrows with each ui an arrow of Ai, de ne ( (u))i = ui. Notice that satis es (E1) and (E2) by construction. For (E3), condition 3 of the de nition of n guarantees that the required equations hold (both Puts yield the very same tuple of arrows as, respectively, an arrow of S1 and an arrow of S2).
Proof. Suppose L and K are given by spg-lenses Li = (gi; pi) where gi : S / Ai, and Ki = (hi; qi) where hi : T / Ai. Without loss of generality, it su ces to assume that L spg K are equivalent by a functor : S / T satisfying conditions (E1)-(E3). The corrs of ML are the objects of S and the corrs of MK are the objects of T. Let the relation be the object function of . We need to show that satis es conditions 1-3 of De nition 13. By (E1) commutes with the Gets so is compatible with the 's (condition 1). Since on objects is a surjective function, is total on both sides (condition 2). For condition 3, suppose S T , so (S) = T , and : Ai / A0i is an arrow of Ai. Then for j 6= i, in the notation of the construction, and writing q for the propagation constructed using q qiTj ( ) = = = = hj (qiT;b( )) hj ( piS;b( )) gj (piS;b( )) piSj ( ) For the amendments, qiTi( ) = qiT;a( ) = piS;a( ) = piS;i( ). And nally, the resulting corrs are related since qiT ( ) = = = d1(qiT;b( )) d1( piS;b( ))
The two constructions between n-ary symmetric lenses and n-wide spans of spg-lenses are closely related. Indeed, one composite of the two constructions is actually the identity. The other is, up to spg equivalence, the identity (up to equivalence because when we start and end with a wide span, the arrows of the head are replaced by the formal sequences described above).
and for any n-wide span L of spg-lenses Li = (gi; pi) where gi : S / Ai, M = M(LM ) L
spg L(ML) Proof. For the rst equation, by inspection, the corrs and 's of MLM are those of M . Further, it is easy to see that the propagations of MLM are identical to those of M .
For the second, the equivalence, notice rst that the head of the original wide span, L, is included by an identity on objects functor into the head S of the wide span L(ML). Using the notation of the construction, the functor sends an arrow s of S to the tuple of arrows (gis). Call that functor . It certainly commutes with the Gets (by construction) and it is identity on objects, and so certainly surjective on objects, so satis es conditions (E1) and (E2). To see that it also satis es condition (E3), and so provides the equivalence required, it su ces to recall that every Put in L(ML) is obtained from the n di erent Gets of the corresponding Put in L, and so carries the latter Put to the former Put, as required.
and spg equivalence classes of n-wide spans of spg-lenses. n equivalence classes of n-ary symmetric lenses
The remainder of this paper will focus on n-wide spans of spg-lenses. 6
We are now going to use the composite of spans de ned in Proposition 10 to de ne several composites of suitable wide spans of spg-lenses. The composites will take place over a single foot common to both spans. Each wide span will have a speci ed closed leg, its left-most leg, and the composites will be de ned using the closed left-most leg of the second wide span.
We will denote an n-wide span L with the left-most leg, (g1; p1) : S / A1 assumed to be closed as follows. A1 zvv(gv1v;vpv1v)vvvvvv (vg2S;p22VM)MVM2V2M2V(MVgM3VM;MVpMV3M)VMVMVMVMMVMVMVMV(gV2V;VpnV)VVVVVVVVVVVVVV+ An 2222
2A2 & A3 : : :
When we de ne one of the composites of two such wide spans L and M say, we will compose (as in Proposition 10) across the left-most leg of the right span M and the i-th leg (i > 1) of the left span L and call it the i-composite. See the diagram below in which (to avoid clutter) the legs of the left span after position i are not shown.
(vkv;vrv)vvvvvvv
U MMMMMMMMM(MmM;MsM)MMMMM A1 zvv(gv1v;vpv1v)vvvvvv(vg2S;p222zvM2)vM22vM22M22MM:M: M(:gMiM;MpMi)MMM:M: :
A2 & Ai = A01 zvvv (g10;p01)vvvvv vvvv v& T22VMMVMV2M2V2(MVgM30VM;VpMV03M)VMVMMVMVMVMV:MV:M(:VgVn0V0;VpV0nV0)VVVVVVVVVVVVV+ A0n0
222 (g20;p02) 2
A02 & A03
Suppose that all the lenses are spg-lenses and that the two left-most legs, (g1; p1) and (g10; p01), are closed. Proposition 10 shows that (m; s) is an spg-lens and that (k; r) is a closed spg-lens, and so (g1; p1)(k; r) is a closed spg-lens by Proposition 8. That last proposition also ensures that all of the other n + n0 3 composites are spg-lenses.
The following de nition makes the details of the i-composite precise by specifying all the indices, but the reader may simply focus on the diagram in which the resulting wide span is made evident noting only that the legs ending at Ai and A01 do not appear in the composite.
are closed is de ned to be the wide span MiL with head U and closed left-most leg (g1; p1)(k; r) : U / A1. The feet are Bj, for j n + n0 2 where Bj = Aj, for j < i, Bj = Aj+1, for i < j < n, and Bj = A0j n+2, for jn < ij, <(hnj;+qjn)0= (2g.j+T1h;epjle+n1s)e(ks;arr)e, ofobrtaiin<edj b<y nre,naunmdbe(hrijn;gqjs)im=il(agrj0lyna+n2d; pc0jomnp+o2s)i(nmg:; s()h,jf;oqrj)n= (gjj<;pnj)+(k;nr0), f2o.r
Our next goal is to show that we can compose spg classes of wide spans by composing representatives of each class. For that it su ces to show that the equivalence is a congruence for the i-composites just de ned. De nition 22 An n-wide span of spg-lenses L = (S; (Ai; gi; pi)i n) is called a multiary lens if (g1; p1) is closed. Proposition 23 Suppose that L = (S; (Ai; gi; pi)i n), M = (T; (Bi; hi; qi)i (n)) and M 0 = (T0; (Bi; h0i; qi0)i (n)) are multiary lenses. Further, suppose that : T / T0 is a functor satisfying conditions E1-E3 so that M spg
Proof. The diagram below shows some of the lenses in the wide spans L, M and M 0 chosen to include all those that are required to construct representative parts of the composite wide spans. To avoid clutter the other lenses have been omitted.
The top composite span (MiL) of spg-lenses has head U, the pullback (in cat) of gi and h1. Similarly the pullback U0 is the head of the bottom span composite (LM 0). (m0;s0) In order to show the claimed equivalence, we construct a functor 0 : U property of the pullback U0 can be used to de ne 0. / U0. Since h01 m = gik, the universal
Since U and U0 are pullbacks of functors, their objects can be taken to be pairs of objects from S and T, respectively S and T0. Similarly, their arrows can be taken to be pairs. Also k and m, respectively k0 and m0 can be taken to be projections. We can now explicitly describe the action of 0 on an arrow of U as 0(u0; u1) = (u0; u1).
It remains to show that 0 satis es E1-E3.
For E1, gx0k0 0 = gxk since k0 0 = k by the construction of 0. Similarly, we have h0xm0 0 = h0 x by the construction of 0 and the fact that h0x = hx. m = hxm For E2, an object of U0 is a pair of objects from S and T0. Now 0 is the identity on its rst component and , which is surjective on objects, on its second component, hence 0 is surjective on objects.
Condition E3 considers both parts of a Put and here we will consider the amendment part in detail. The
other part is routine and similar to the proof found in [
Suppose U is an object of U and U 0 = 0(U ). Required to show that the amendment for the Put along (hj ; qj )(m; s) into U is the same as the amendment for the Put along (h0j ; qj0 )(m0; s0) into U 0. In both cases the amendment is obtained, according to De nition 7, by composing an amendment from the lens (hj ; qj ) (respectively (h0j ; qj0 )) which we will call a (respectively a0) with hj (respectively h0j ) applied to an amendment for the lens (m; s) (respectively (m0; s0)) which we will call b (respectively b0). Explicitly, a a0 b b0 = = = = qjmaU ( ) qj0ma0U0 ( ) hj (saU (qjmbU ( ))) We will show that a = a0 and b = b0, so that of course the amendments ba = b0a0 as required. a = a0 : a = = = qjmaU ( ) qj0amU ( ) qj0ma0U0 ( ) / T10 be the Put of into m0U 0 and note that = 0 since m0U 0 = m0 0U = b = = = = = = = = = =
Proposition 24 Suppose that L = (S; (Ai; gi; pi)i n), L0 = (S0; (Ai; gi0; p0i)i n) and M = (T; (Bi; hi; qi)i m) are multiary lenses. Further, suppose that : S / S0 is a functor satisfying conditions E1-E3 so that L spg L0, and that L and M (and so also L0 and M ) are composable over some Ai. Then the two wide span composites are equivalent, that is MiL spg MiL0.
Proof. As above, the diagram below shows some of the lenses in the wide spans L, L0 and M chosen to include all those that are required.
The top composite span (MiL) of spg-lenses has head U, the pullback (in cat) of gi and h1. Similarly the pullback U0 is the head of the bottom span composite (L0M ).
(m;s) (gj;pj)S ?o????(?g?i?;pi) (Agj0j; p_?0j?)????? A(gii0?;=p0i)`B1 o
S0 o
We have de ned multiary lenses above as certain wide spans of spg-lenses and noted that we may consider
composites for them when there is a matching condition on the feet. In this section we show how multiary
lenses and their composites may be organised into the structure of a multicategory, a concept rst introduced by
Lambek in the 1960's [
De nition 25 [
(M5) The identity operation is a map 1( ) : C0 / C1 with 1c : c / c. (M6) The composition operation assigns, to each f : c1 : : : cn / c and an n-tuple (fi : !ci composite f (f1; : : : ; fn) : !c1 : : : !cn / c where the source is obtained by concatenating lists.
/ ci; i = 1; : : : ; n), a
In general, for a category with pullbacks, there is a multicategory of wide spans constructed much as we do below. Since the category of spg-lenses (like the category of asymmetric delta lenses) does not have pullbacks, we need to describe the multicategory structure in detail, but the idea is the same as for the case with pullbacks, and to preserve the analogy we will write \pullback" and \wide pullback" below to mean the pullback and wide pullback of the relevant Gets in cat, endowed with Puts in the canonical way described above for pullbacks (for wide pullbacks the constructions can be done a pullback at a time to generate what we are calling the wide pullback of a given collection of closed aa-lenses).
For our multimorphisms we are going to consider egory ML of multiary lenses.
spg classes multiary lenses. We can now de ne a multicatAn object of ML is a category.
A multimorphism f of ML is an ( spg equivalence class of) multiary lenses.
Suppose f = [L] is a multimorphism which is the equivalence class of the multiary lens L = (S; (Ai; gi; pi)i n). The source of f is A2 : : : An and the target of f is A1.
Identity: For any category A1, its identity morphism is the equivalence class of the span (so n = 2) of identity spg-lenses from A1 to A1 The identity spg-lens is closed, so in particular the left leg of that span is closed, as required.
Composition: Suppose that f = [L] is a multimorphism where L = (S; (Ai; gi; pi)i n) is a representative. Suppose also that for 2 i n, fi = [Mi] are multimorphisms with representative multiary lenses Mi = (Ti; (Bij ; hij ; qij )j mi ) satisfying Bi1 = Ai. The composite multimorphism is denoted f (f2; : : : ; fn) : B21 : : : B2m2 : : : Bn1 : : : Bnmn / A1 For representative multiary lenses as above, we obtain a representative of f (f2; : : : ; fn) as follows. We denote the composite of L and Mi at Ai as L i Mi. Denote its head by Ui. Its left leg lens is (Ui; A1; (ki; ri)(g1; p1)). The remaining mi 1 legs are denoted (Ui; (Bij ; kij ; rij )2 j mi ) where (kij ; rij ) = (hij ; qij )(mi; si). The head of the composite representative is the wide pullback V of the (g1; p1)(ki; ri) (which are all closed). Its left leg is the common (closed) spg-lens from V to A1. The spg-lens from V to Bij is the composite of the projection lens from V to Ui followed by (kij ; rij ) to Bij .
Consider the following diagrams showing rst how we de ne Ui:
(kviv;rviv)vvvvvvv Ui MMMMMMMM(MmMiM;MsMi)MMMM A1 zvv(gv1v;vpv1v)vvvvvvv S zMvvMvMMMMMM(MgMiM;pMiM)MMMM
& Ai = Bi1
& (zvhviv1v;qviv1v)vvvv(vhvi2T;qii222MV)22MV22MV2(2MhV2MiV3MV;MqVMiM3V)MVMVMVMVMVM:VM(:MVh:&VimViV;VqVimViV)VVVVVVVVVVV+ Bimi
Bi2 Bi3 and next, showing how we de ne V and the legs of the composite multiary lens, but with only U1 and U2 displayed to minimise the complexity of the diagram: zvvvvvvvvvvvvvv
V MMMMMMMMMMMMMMMMM
& A1 rzfvvfffffffffffUff122f?2M?f?MfM22fMf?M?fM?MfMfMfMfMfMfMMfMfMffffffffffffffff U222MVMVMVMVMVMVMVMVMVMVMVMMVMVMV(MkV2VmViV;Vr2VmVV2)VVVVVVVVVVV+ B2m2 : : : (g1;p1)(vkv1v;rv1v)vvvvvv 222??2? ?? & (k22;r22)2222222 &
B12 B13 : : : B1m1 B22 B23 : : :
It remains to show that f (f2; : : : ; fn) is independent of the representative multiary lenses chosen.
Proof. The independence of representatives follows immediately from Propositions 23 and 24 applied to the diagram above.
of multiary lenses. 8
We begin the discussion with a few words about why we have excluded from our de nitions what Diskin et al [
We have taken the view that, instead, engineers, immersed in their application environment and knowing what is and isn't desirable in that environment, can choose from among the lenses that the mathematics, without K, o ers.
There are further technical reasons for excluding K at this stage too. Having K as part of a model space de nition would mean that the correct K needs to be chosen in the domain of an amendment lens, and yet K plays no role at all when it is in the domain of an amendment lens. So, apparently reasonable lenses only become problematic when one goes to compose them with other apparently reasonable amendment lenses and nds that their Ks are incompatible. But in many cases those incompatible Ks were never relevant to the original lenses at all. It is better to be rid of the Ks and instead to let the user choose not to use lenses that they would want to exclude from being legitimate lenses. Having K be part of the model spaces adds complexity to de ning composition (one of the principal challenges confronted in this paper) in ways that seem inessential.
Furthermore, when it comes to forming compositions that require \pullbacks" as in Proposition 10, K can have more deleterious e ects. In the notation presented there, compatibility relations that occur in the heads of the spans S and T have no relevance to the four input lenses, but need to be used to de ne U, which in turn may be involved in further compositions.
In short, it seems better at this stage to study aa-lenses that don't require any extra relations K, and allow users to choose from among them. If an aa-lens does something that a user might not want to have, and might exclude via a judicious choice of K, that user can just choose those lenses that do not exhibit the undesirable behaviour. This is important because what is undesirable in some applications may not be undesirable in others, and trying to capture it as part of the lens structure, or even worse as part of the model space structure limits possible compositions and can have severe e ects on the existence of \pullback" amendment lenses.
Another way of viewing what we are doing here in excluding K might be to say that the compatibility relation is simply the composability relation { every composable pair is compatible.
Next a few words about our use of closed left legs.
All cospans of d-lenses that satisfy PutGet have \pullbacks", and so can be used to de ne composites of symmetric d-lenses. A natural plan on moving to aa-lenses might be to calculate similar \pullbacks". But there is a serious problem. As can be seen in the de nition of the amendment sa in Proposition 10, the fact that (h; q) is not closed complicates de ning the amendment for its \pullback" (m; s) resulting s(aS;T )( ) = p0T 0 (qaS (g0( ))) = ~b b say. But if the other leg of the cospan, (g0; p0), were also not closed, then (qbS (g0( )); ~b ) would not necessarily be an arrow of U and the S component would need to adjusted by a similar further amendment, which would in turn require further adjustment of the amendment in T, potentially, ad in nitum. In short, composing across a pair of non-closed legs can cause havoc.
Of course, which leg in a cospan is closed has no relevance for the existence of the \pullback". But we do need to be consistent in our choice, and we have chosen the left leg to be the closed leg.
Also of course, but worth remarking, if both legs are closed then the calculations in the proof of Proposition 10
are the same as the calculations for the usual \pullback" of d-lenses [
There is an interesting similarity between spans of spg-lenses with closed left leg, and the symmetric lenses
studied in the paper by Fong and Johnson [
Finally, a remark about our construction of the multicategory of multiary lenses summarised in Corollary 27. We have given in the preceding section a fairly explicit account of the multicategory composition of n+1 multiary lenses because that is what's required for a general composition in a multicategory. Meanwhile, it is worth noting that using just the identity and associativity axioms for multicategories gives a coherence result which shows that general multicategory compositions can always be constructed from compositions with at most two nonidentity multiarrows, that is, multiarrows of the form f (1; 1; : : : ; 1; fi; 1; : : : 1) | these are in a sense the binary multiarrow compositions. An alternative approach to obtaining Corollary 27 is to de ne those binary multiarrow compositions to be the composite given in each case by De nition 21, and then appeal to the coherence result to obtain the general multicategory compositions. 9
This paper has aimed to lay the foundations for work on multiary lenses, whether in the \propagation" form (in
the style of the original symmetric lenses [
With those foundational matters settled the paper turns to the question of how multiary lenses should be composed, and what algebraic structure they and their composites might form. Aiming for broad generality, we have worked with wide spans of aa-lenses, and shown how to de ne composites for those wide spans with a closed left leg. Finally we demonstrate that those multiary lenses form a multicategory using the composites calculated across their closed legs.
A nal word about the title: Why the plural (Multicategories of Multiary Lenses)? We want to emphasise that while we have isolated general classes of lenses that interact well and through their generality promise wide applicability, we have also determined that adding many kinds of extra requirements to those lenses, for example, that the component lenses are all closed, or that they satisfy (Re ect0) or (Re ect0*), we still obtain a multicategory of such lenses. Furthermore, for workers who might have in mind certain compatibility relations K, something that we have excluded from the analysis presented here, it is possible to look at submulticategories of the multicategory of multiary lenses that contain those lenses that they consider acceptable for their application.
We especially want to emphasise that the work that began this study of multiary lenses, work which was based on wide spans of d-lenses, is just a special case of the results nally presented here. The authors are grateful for the support of the Australian Research Council, the Centre of Australian Category Theory and Mount Allison University. Much of what is presented here grew out of work begun at Schloss Dagstuhl and we gratefully acknowledge their support.