I'll describe a transformation, (U|T:V), as practical for compositions * (in U) and % (in V) - so U= ((|*)| y in (|*(x)), x->y :) and V= ((|%)| y in (|%(x)), x->y :) - precisely if, whenever f = w*...*a in U, there are arrows p, q in V with q % T(a) = T(f) = T(w) % p. (So the image of a composite can be factorised via the images of its first and last components.)
I'll describe a pair of practical transformations, [S, T], each in {(U|:V)} as (fully) conjoinable with respect to a pair of (factorising) compositions, * on U and % on V, precisely if [S, T] is preConjoinable in {transform (U|:V)} and `[f, g] and [x, y] in Composable(U) with f*g = x*y' &implies; S(f)%T(g) = S(x)%T(y). [Note that composability of [Sf, Tg] and [Sx, Ty] follow from preConjoinability of [S, T].] I usually won't bother to use different symbols for the two compositions - I'll call them both &on; unless there's a real need to emphasise the distinction.
In this case we are able to define a conjoint transformation, (U| S*T :V), given by: for each f in Arrow(U), pick [g, h] in Composable(U) for which f = g&on;h; then (S*T)f = Sg&on;Th, the latter composition being done in V, the former in U. Given the definition of (full) conjoinability, this has the same value for every factorisation of f.
Observe that [S, T] is conjoinable with respect to given compositions precisely if [dual-T, dual-S] is conjoinable with respect to the duals of the compositions on U and V. In this case the two conjoints satisfy dual-(S * T) = dual-T * dual-S. (Here, dual-S and dual-T are just S and T viewed as transformations (dual-U|:dual-V).)
Consider now a collection of transformations on a collection of arrow worlds, each with a composition. If it forms an arrow world under the natural composability of transforms, then that natural composition is, indeed, a composition on the arrow world of transforms. Likewise, if the collection of transformations forms into an arrow world under (full) conjoinability, then conjoining acts as a composition on this arrow world.
If such a collection of transformations forms an arrow world under both composition and conjoining, then I shall call it a transform world.
Given this definition of conjoining for transformations, look now for the corresponding structure for coTransformations. One coTransformation, (A|T:W), is pre-contrajoinable after another, (A|R:W), precisely when `f composable before g in A implies `R(g) composable before T(f) in W'. In other words, if g&on;f is a valid composition in A, then T(f)&on;R(g) is valid in W. The conjoint T*R (defined in terms of T, S being transformations (dual-A|:W), as is their conjoint) has T*R(g&on;f) = T(f)&on;R(g). Again merely to emphasise that T and R are coTransformations, I'll refer to T*R as the contrajoint of T after R (or of R before T).
If we have two transformations, S and T, conjoinable in {(U|:V)}, with U identifiable, then if either S or T respects identities (ie its image of any identity is an identity) the conjoint, S * T, is equal to the other. Furthermore, this implies that, in this context, in a conjoinable pair of transformations each of which respects identities, the two transformations are equal (and equal to their self-conjoint).
A functor is a transformation, F, which is self-conjoinable and for which, whenever it is conjoinable with a transformation, T, the conjoint is equal to that transformation, F * T = T or T * F = T as appropriate. Thus functors are identities for conjoinability in transform worlds.
A functor (C|F:D) is said to begin (end) a transformation (C|T:D) precisely if [T, F] ([F, T]) is conjoinable with respect to the compositions on C and D. In this case, the conjoint is equal to T, by the definition of F. Every functor begins and ends itself. A transformation, T, is said to be natural [a natural transformation] for a pair [F, G] of functors precisely if G begins T and F ends T.
Written by Eddy.