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.

$Id: conjoin.html,v 1.2 2001-10-17 17:11:30 eddy Exp $