Let us commence by introducing the local formalism that constitutes the basis of Badiou’s own, ‘calculated phenomenology’. Badiou is unwilling to give up his thesis that the history of thinking of being (ontology) is the history of mathematics and, as he reads it, that of set theory. It is then no accident that set theory is the regulatory framework under which topos theory is being expressed. He does not refer to topoi explicitly but rather to the so called complete Heyting algebras which are their procedural equivalents. However, he fails to mention that there are both ‘internal’ and ‘external’ Heyting algebras, the latter group of which refers to local topos theory, while it appears that he only discusses the latter—a reduction that guarantees that indeed that the categorical insight may give nothing new.

Indeed, the external complete Heyting algebras T then form a category of the so called T-sets, which are the basic objects in the ‘world’ of the Logics of Worlds. They local topoi or the so called ‘locales’ that are also ‘sets’ in the traditional sense of set theory. This ‘constitution’ of his worlds thus relies only upon Badiou’s own decision to work on this particular regime of objects, even if that regime then becomes pivotal to his argument which seeks to denounce the relevance of category theory.

This problematic is particularly visible in the designation of the world m (mathematically a topos) as a ‘complete’ (presentative) situation of being of ‘universe [which is] the (empty) concept of a being of the Whole’ He recognises the ’impostrous’ nature of such a ‘whole’ in terms of Russell’s paradox, but in actual mathematical practice the ’whole’ m becomes to signify the category of Sets – or any similar topos that localizable in terms of set theory. The vocabulary is somewhat confusing, however, because sometimes T is called the ‘transcendental of the world’, as if m were defined only as a particular locale, while elsewhere m refers to the category of all locales (Loc).

An external Heyting algebra is a set T with a partial order relation <, a minimal element μ ∈ T , a maximal element M ∈ T . It further has a ‘conjunction’ operator ∧ : T × T → T so that p ∧ q ≤ p and p ∧ q = q ∧ p. Furthermore, there is a proposition entailing the equivalence p ≤ q iff p ∧ q = p. Furthermore p ∧ M = p and μ ∧ p = μ for any p ∈ T .

In the ‘diagrammatic’ language that pertains to categorical topoi, by contrast, the minimal and maximal elements of the lattice Ω can only be presented as diagrams, not as sets. The internal order relation ≤ Ω can then be defined as the so called equaliser of the conjunction ∧ and projection-map

≤Ω →^{e} Ω x Ω →_{π1}^{∧} L

The symmetry can be expressed diagrammatically by saying that

is a pull-back and commutes. The minimal and maximal elements, in categorical language, refer to the elements evoked by the so-called initial and terminal objects 0 and 1.

In the case of local Grothendieck-topoi – Grothendieck-topoi that support generators – the external Heyting algebra T emerges as a push-forward of the internal algebra Ω, the logic of the external algebra T := γ ∗ (Ω) is an analogous push-forward of the internal logic of Ω but this is not the case in general.

What Badiou further requires of this ‘transcendental algebra’ T is that it is complete as a Heyting algebra.

A complete external Heyting algebra T is an external Heyting algebra together with a function Σ : PT → T (the least upper boundary) which is distributive with respect to ∧. Formally this means that ΣA ∧ b = Σ{a ∧ b | a ∈ A}.

In terms of the subobject classifier Ω, the envelope can be defined as the map Ω^{t} : Ω^{Ω} → Ω^{1} ≅ Ω, which is internally left adjoint to the map ↓ seg : Ω → Ω^{Ω} that takes p ∈ Ω to the characteristic map of ↓ (p) = {q ∈ Ω | q ≤ p}27.

The importance the external complete Heyting algebra plays in the intuitionist logic relates to the fact that one may now define precisely such an intuitionist logic on the basis of the operations defined above.

The dependence relation ⇒ is an operator satisfying

p ⇒ q = Σ{t | p ∩ t ≤ q}.

(Negation). A negation ¬ : T → T is a function so that

¬p =∑ {q | p ∩ q = μ},

and it then satisfies p ∧ ¬p = μ.

Unlike in what Badiou calls a ‘classical world’ (usually called a Boolean topos, where ¬¬ = 1_{Ω}), the negation ¬ does not have to be reversible in general. In the domain of local topoi, this is only the case when the so called internal axiom of choice is valid, that is, when epimorphisms split – for example in the case of set theory. However, one always has p ≤ ¬¬p. On the other hand, all Grothendieck-topoi – topoi still materially presentable over Sets – are possible to represent as parts of a Boolean topos.