Let C be a category with finite products, and let F : C -> C be a functor, along with a natural transformation F*(X,Y,Z) : hom(X x Y, Z) --> hom(X x FY, FZ) that preserves composition and identities in the appropriate manner. (The idea is that this gives a behaviour for F on collections of arrows from Y to Z indexed by X.) Does anyone have a name for a functor with such a natural transformation? Note that if C is cartesian closed, then this is the same as having a natural transformation from Y^Z to (FY)^(FZ) that preserves composition and identities. This sort of functor arises in logic as follows: Let A[X] be a formula with a positively occuring propositional variable X. Then B |- C ------------ A[B] |- A[C] is a derived rule, making A[-] into a functor. But we can also do this with additional side formulae: D, B |- C --------------- D, A[B] |- A[C] giving a natural transformation as described as above. I'd use the term "internal functor", except that this is already used for a functor between two internal categories. Ralph Loader. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++