Consider a realizability topos RT(A) over some PCA A. There is an embedding Nabla : Set -> RT(A), which takes a set X to the assembly whose underlying set is X and the existence predicate is trivial, i.e., every element of X is realized by every realizer of A. Let [n] = {0, 1, 2, .., n-1} be the set with n elements. I have some interest in the subobject of Nabla([n]) whose underlying set is [n] and the existence predicate is E(0) = { numeral(0) } E(1) = { numeral(0), numeral(1) } ... E(k) = { numeral(k-1), numeral(k) } ... E(n-1) = {numeral(n-2)} In words: there are n elements 0, 1, 2, ..., n-1, where two consequtive elements share a realizer. The question is; is this object definable in the internal language of the topos? Note that Nabla(2) is definable as the object of not-not-stable truth values, and that each Nabla(X) is also definable with a bit more work. With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]