  Any topos may be conceived as possible “universe of discourse” in which mathematical assertions may be interpreted and mathematical constructions may be performed. Mathematical assertions are rendered interpretable in a topos  E  by expression within  E's internal language — a type-theoretic version of the usual language of set theory. In a manner analogous to Boolean-valued validity, one can introduce an appropriate notion of validity in  E  of a sentence σ of its internal language. Again, we write  E   ⊨ σ for “σ is valid in  E”.