Cardinality of the set of truth values in a Heyting-valued model of IZF I've very recently become interested in intuitionistic set theory. I'm now trying to get acquainted with the very basics, and I have a number of small silly questions, that might not make sense due to my current lack of knowledge (apologies if that's the case).

Can the cardinality of the set $\Omega$ of truth values/subobject
  classifier in a Heyting-valued model of intuitionistic ZF be defined
  (internally to the model)? 
If so, can it be different from 2? And does it coincide with the
  cardinality of $\Omega$ as an ordinary set?

For example, taking $\Omega$ as the Heyting algebra from the third example here, would its internal cardinality be 2, 3 or undefined?
I've found this article that claims that the cardinality cannot generally be defined in constructive mathematics except for a special type of decidable sets, but the article doesn't go into much detail as to why; it only rules out the existence of a map assigning the cardinality 1 to singletons.
 A: Welcome to the wondrous world of intuitionistic set theory!
I don't know your definition of cardinality; mine is: Sets $X$ and $Y$ are of the same cardinality if and only if there exists a bijection $f : X \to Y$. This defines an equivalence relation on the universe; the equivalence classes are called cardinal numbers.
With this definition, every set $X$ has a cardinality, namely the cardinal number represented by $X$ itself. However, in the absence of the law of excluded middle, and to a lesser extent in the absence of the axiom of choice, the thusly-defined cardinal numbers might not enjoy the properties you might expect from them. In particular:


*

*The relation defined by setting $[X] \leq [Y]$ if and only if there exists an injection $f : X \to Y$ might not be a linear order.

*The relation defined by setting $[X] \geq [Y]$ if and only if there exists a surjection $f : X \to Y$ might not be the opposite of the relation $({\leq})$.

*Subsets of sets of the form $\mathbf{n} = \{0,1,\ldots,n-1\}$ might not be of the same cardinality as any $\mathbf{k}$.


Yes, it can happen that $\Omega$, the powerset of the singleton set, is not of the same cardinality as $\mathbf{2} = \{ 0,1 \}$ (whose cardinality is traditionally called "$2$"). The set $\Omega$ is of the same cardinality as $\mathbf{2}$ if and only if the law of excluded middle holds.
Regarding the third Wikipedia example you linked to: Let $H$ be the Heyting algebra of that example. Let $X$ be the locale which has $H$ as frame of opens. We can then build the topos $\mathrm{Sh}(X)$ of sheaves on $X$. This topos will contain a subobject classifier (a certain sheaf), traditionally written "$\Omega$". As with any topos, this topos has an internal language which we can use to reason about the objects and morphisms of the topos in a naive element-based way. From the internal point of view, $\Omega$ is just a set (not a sheaf), and in fact it is the powerset of the singleton set. Like any set, it has some well-defined cardinality. A formalization of your question is: What is this cardinality? Well, $\Omega$ is neither of the same cardinality as $\mathbf{2}$ nor of the same cardinality as $\mathbf{3}$. It still has some cardinality though, trivially so.
Please feel free to ask for clarifications!
