Names for these (di)natural transformations?

Names for these (di)natural transformations?

[Mike Stay]

Some monads on Set have algebras that can be thought of as data
structures labeled by elements of a set.  For example, the free monoid
on a set X can be thought of as the collection of finite lists whose
elements are in X.

The list monad T has a tensorial strength, a transformation
    t_{X, Y}: X x TY -> T(X x Y),
natural in X and Y.  The strength pairs x with each element of the list M:
    t_{X, Y}(x, M) = T( y |-> (x, y) )(M).

There are other transformations for which I'd like to know names and
what coherence laws they have to satisfy.

The first is a transformation
    u_{X, Y}: T(X x Y) -> (X -> TY),
natural in Y and dinatural in X.  In the case of lists,
    u_{X, Y}(M) = x |-> flatten( T( (x',y) |-> [y] if x = x', []
otherwise )(M) ).
That is, it filters out those pairs in M that do not have x as the
first element of the pair and lists the second elements of the pairs
that do.

The second is a transformation
    v_{X, Y}: T(X -> Y) -> (X -> TY)
natural in X and Y.  In the case of lists,
    v_{X, Y}(M) = x |-> T( f |-> f(x) )(M) ).
That is, it applies each f in M to x.

I've worked out a few of the coherence laws relating these three
transformations, but I'd like to be sure I haven't missed any.
-- 
Mike Stay - metaweta@gmail.com
http://www.math.ucr.edu/~mike
http://reperiendi.wordpress.com


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]