Richard Wood mentioned an observation about functions Omega->Omega in a topos. In the more abstract situation of a classifier Sigma for some subclass of monos (closed under isomorphisms, composition and pullback along arbitrary maps, and such that the characteristic function of a subobject, where it exists, is unique), the following formula holds: for any function f:Sigma x X -> X and predicate a:X -> Sigma f(a) & a = f(true) & a In fact, along with Sigma being a semilattice, this is necessary and sufficient for Sigma and its powers to form a full subcategory of some category in which Sigma is a classifier. I wonder whether anyone has noticed this formula before? In my construction, the Frobenius law for an existential quantifier is derivable from it. It is also reminiscent of the Berry order in stable domain theory, but I can see no substantial connection. It is easily provable in higher order logic: either way, assume a, so a=true. Curiously, Phoa's Principle (in synthetic domain theory) is the conjunction of the higher order equation above its lattice dual f(a) \/ a = f(false) \/ a and all functions f:Sigma->Sigma are monotone. For the continuation of this story, go to Vancouver ... Paul