Dear all, 1) not(CH) I'm reacquainting myself with the proof using toposes that not(CH) is relatively consistent. There's one step that is not quite as I'd like it, and that is as follows. Let P be a poset with the countable chain condition and the double negation topology (or indeed any site where all covering sieves are generated by families that are at most countable), then for objects X,Y in the base topos S that are infinite (in the sense that N x X = X), having Epi(Y,X) = 0 in S implies that Epi(Y^,X^) = 0 in Sh(P). It seems to me that the proof, as recounted in Mac Lane--Moerdijk or Johnstone's Baby Elephant for instance, uses LEM, by assuming that Epi(Y^,X^) =/= 0 and showing that Epi(Y,X) =/= 0. I haven't thought this through, but it seems like it might be possible to rework things so that the proof in fact shows that from an isomorphism 0--> Epi(Y,X) one can show that any two maps Epi(Y^,X^) --> \Omega are equal, and hence since 0 --> Epi(Y^,X^) is a subobject, it must be an isomorphism. Has anyone thought about this before? Of course, the previous paragraph may be nonsense, I admit... 2) Cardinal inequality in the absence of LEM This does raise the related question as to what the definition or definitions of <, strict inequality of cardinalities (i.e. just sets), could be in the absence of LEM and still be useful. If one were to adopt the following: Definition: B < A if and only if there a mono B >--> A and a factorisation B >--> A' >--> A such that Epi(B,A') = 0. then---modulo the issue in part 1)---the existing proof of the preservation of inequalities of sets seems to work without the assumption the base topos is boolean (which is needed in the existing proof to find a retract A -->> A' ). In the presence of LEM the definition of < reduces to the usual one, but I don't see a good reason or philosophy to single out this particular definition over other potential definitions except that it is what the proof uses. Thoughts? Best regards, David [For admin and other information see: http://www.mta.ca/~cat-dist/ ]