Dear categorists, I am trying to wrap my mind around the concept of an (internal) chain-complete poset in a sheaf topos. I am failing to come up with an example of a poset that is chain-complete but is not complete. The precise definitions of "chain-complete" in the internal language are as follows. Suppose (P, <=) is a poset in a topos. For C in Omega^P, let chain(C) be the statement forall x, y : P, (x in C and y in C) ==> (x <= y or y <= x) Then P is chain-complete if forall C : Omega^P, chain(C) ==> exists x : P, x is the supremum of C where "x is the supremum of C" means the usual thing. So what does a chain-complete poset which isn't complete look like? Since I am used to arguing intuitionistically, it would help a lot if there were some (possibly infinitary) logical principle or schema that is typical of sheaf toposes -- something expressing the local nature of validity. Such a principle ought to be invalid in realizability toposes, so perhaps it should express or imply cocompleteness (with respect to Set). But would that be of any help for arguing in the internal language? With kind regards, Andrej Bauer [For admin and other information see: http://www.mta.ca/~cat-dist/ ]