Does anyone know an example of a a topos E with nno validating internal countable choice (ICC), i.e. (-)^N preserves epis, such that some booleanization of E doesn't validate (ICC) anymore? In particular I am interested in the case where E is a relative realizability topos induced by a pca A together with a sub-pca A_#. For a particular such case I managed to answer the question positively (see https://lmcs.episciences.org/4129/pdf) using a variant of Spector's bar recursion. But I don't know the answer when I make the underlying pca's of loc.cit. effective. Another situation where I also don't know the answer is KV_{\neg_U\neg_U} where KV is the Kleene-Vesley topos (see Jaap van Oosten's book) and U is {\tau} where \tau decides the halting problem. I think - or rather hope - that in these two latter cases booleanization does not preserve (ICC). But for already quite some time I failed to prove this. Only recently I realized that I don't know any example where booleanization does destroy (ICC). So I would be very glad to learn about such an example. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]