[Note from moderator: apologies to Dusko for prepending nonsense to his post, regards, Bob] Uday S. Reddy:
Consider a monoid <M,*,1> in a CCC. The operations of interest are natural transformations E_A : [A => M] -> M that satisfy the following equations (in the internal language of the CCC):
1) E_A(\lambda x. 1) = 1 2) E_A(\lambda x. a * g`x) = a * E_A(g) 3) E_A(\lambda x. g`x * a) = E_A(g) * a 4) E_A(\lambda x. E_B(\lambda y. h`x`y)) = E_B(\lambda y. E_A(\lambda x. h`x`y))
The naturality of E_A in A seems to be a very strong requirement (provided that am not misuncerstanding anything, ofcourse). Let T the terminal object (since 1 already denotes the unit of M). Equations (1) and (2) imply E_T(\lambda x. a) = a, so E_T is iso. The naturality, on the other hand, implies that for every a,b : T --> A holds a=>M ; E_T = E_A = b=>M ; E_T Such E_A, I think, shouldn't be thought of as a quantifier: modulo E_T, it actually boils down to the *evaluation* at (ie substitution of) an arbitrary global point of A: E_A(g) = g`a = g`b Instanciating A = M and g = \lambda x. x yields a = 1, ie 1: T --> M is the only global point of M. If T generates, M is T. On the other hand, if there is an initial object 0 in the CCC, the naturality in A implies that all E_A are constantly 1... Without the naturality, conditions (1--4) seem to be rather easy to satisfy. For a fixed A, conditions (2) and (3) are a kind of naturality on E_A itself. To make this precise, define on A=>M the pointwise monoid structure g * h = \lambda x. g`x * h`x Thinking of M and A=>M as categories, each with one object *, we have the Hom-functors from M^op x M and from A=>M^op x A=>M to the CCC where they live. On the other hand, there is the monoid morphism I : M ---> A=>M m |--> \lambda x. m which can be construed as a functor. Precomposing Hom_{A=>M} with I^op and I, we get a functor from M^op x M. Conditions (2) and (3) are now exactly the naturality of E_A : Hom_{A=>M} (I*, I*) ---> Hom_M (*,*) in each of the arguments. Hom_M thus appears as a retract of the functor Hom_{A=>M} o (I^op x I)... All together, E_A thus appear as a weak kind of *abstraction operators* (like in www.cogs.susx.ac.uk/users/duskop/papers/CLNA.ps.gz). All this may not be enlightening at all, but it does seem to help pin down the models: eg, evaluations/substitutions of the arbitrary points will work again, as well as, when M is a complete lattice, the infima and the suprema, corresponding to the quantifiers... (No naturality in A, ofcourse.) Apologies if I got carried away a bit. It's a nice question. I hope others will tell more. Regards, -- Dusko Pavlovic