Re: Naturality Squares and Pullbacks

[Barry Jay <cbj@socs.uts.edu.au>]

>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