In studying Algol-like languages, I repeatedly run into operators that have an interesting structure. I am wondering if such operators are studied somewhere. 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): E_A(\lambda x. 1) = 1 E_A(\lambda x. a * g`x) = a * E_A(g) E_A(\lambda x. g`x * a) = E_A(g) * a E_A(\lambda x. E_B(\lambda y. h`x`y)) = E_B(\lambda y. E_A(\lambda x. h`x`y)) These operators "feel" like existential quantifiers. In fact, if M is a subobject classifier with the monoid structure ofh conjunction, then the existential quantifier E satisfies all of these equations (though it is not a natural transformation). In the applications I am interested in, M is a type of commands, with * as sequential composition and 1 as the null action. An example of E is a local variable declaration. Is there some algebra or theory related to these kinds of operators? Cheers, Uday Reddy