A natural transformation is an indexed family of arrows such that a certain diagram commutes. One could require a stronger condition, namely that the said diagram is a pullback. What would such a transformation be called? I'm sure I've seen this in the literature before but I cant remember where. Pointers?
Cartesion natural transformations data:F=>L into the list functor have been used to represent the data-shape decomposition of many data types of the form FX. data_X FX --------> LX | | | F! = | | | L! = shape |-- | length | | F1 --------> L1 data_1 = arity Examples include tree types and array types. See, for example @Article{Jay95b, Author= cbj, Title={A semantics for shape}, Journal={Science of Computer Programming}, Volume=25, Year={1995}, Pages={251--283} } and other papers at http://linus.socs.uts.edu.au/~cbj.
This problem arose in the context of finitary monads where T(X) is the derived operations over a set X for some signature. The naturality square for the unit turns out to be a pullback. This then implies that the unit of the monad is a monic - presumably this is a result in the literature somewhere. Again, pointers?
Neil Ghani
If T(X) = mu_Y. X + P(X,Y) for some polynomial P then the cartesian-ness of the unit for the monad follows from one of the main theorems of the paper above, which shows that taking initial algebras preserves cartesian-ness. Here it is applied to the (cartesian) inclusion X -> X + P(X,Y). Barry Jay | Associate Professor C. Barry Jay www: linus.socs.uts.edu.au/~cbj | Reader in Computing Sciences ftp: ftp.socs.uts.edu.au/Users/cbj