Elementary topos theory

Almost all of mathematics can be carried out inside the category $\cat{Set}$ of sets and functions. Which features of $\cat{Set}$ does it actually use? Three stand out:

1. we can form finite limits — products, solution sets of equations, inverse images;
2. we can form function sets $Y^X$, and functions of two variables correspond to functions into function sets;
3. subsets are the same as predicates: a subset $A \subseteq X$ is the same thing as its characteristic function $\chi_A : X \to \{0, 1\}$.

Around 1969–70, F. William Lawvere and Myles Tierney took these three features as axioms for a category. The result, an elementary topos, turned out to describe a remarkable range of "universes of sets": sheaves on a topological space, sets equipped with a group action, sets that vary along stages of knowledge, a universe in which every function $\N \to \N$ is computable. Mathematics can be done inside each of them — but in most of them the logic is intuitionistic: a statement can be "true on part of the space", and the law of excluded middle need not hold.

About a decade earlier Alexander Grothendieck had reached the same objects from algebraic geometry, as the right notion of "generalised space" for cohomology. Topos theory is where these two lines meet. This lesson builds on categorical logic (cartesian closed categories, Heyting algebras), limits and the Yoneda lemma.

Take a very small space, the Sierpiński space $S = \{a, b\}$ whose open sets are $\varnothing \subset \{a\} \subset S$. A sheaf $F$ on $S$ amounts to a set $F(S)$ of global sections, a set $F(\{a\})$ of sections over the open point, and a restriction map $F(S) \to F(\{a\})$. (The empty open set contributes a single section, and no cover of $S$ omits $S$ itself, so there is no gluing condition.)

So consider a set $A_1$ ("sections over the whole space"), a set $A_0$ ("sections over the open point") and a map $\mathrm{res} : A_1 \to A_0$, together with a sub-collection: subsets $S_1 \subseteq A_1$ and $S_0 \subseteq A_0$ with $\mathrm{res}(S_1) \subseteq S_0$. For a global section $x \in A_1$, how true is "$x \in S$"? There are three possibilities:

• $x \in S_1$: true everywhere;
• $x \notin S_1$ but $\mathrm{res}(x) \in S_0$: true on the open point $\{a\}$ only;
• $\mathrm{res}(x) \notin S_0$: true nowhere.

The truth value of "$x \in S$" is the open set on which it holds: $S$, $\{a\}$ or $\varnothing$. In $\cat{Set}$ — sheaves on a one-point space — only "everywhere" and "nowhere" are possible, and we get the familiar two truth values.

Topos theory takes this seriously: an object $\Omega$ of truth values, whose "elements" may be partial truths, and a logic computed from it.

Throughout, $\mathcal{E}$ is a category with finite limits; $1$ denotes a terminal object.

Combining (2) and (3) gives power objects $PX = \Omega^X$ with $\mathrm{Sub}(Z \times X) \cong \mathcal{E}(Z, PX)$; a classical theorem says that "finite limits + power objects" is an equivalent definition. Finite colimits are not assumed: Robert Paré (1974) proved that they follow, because the functor $P = \Omega^{(-)} : \mathcal{E}^{\mathrm{op}} \to \mathcal{E}$ is monadic.

Now fix a small category $\cat{C}$ and write $\widehat{\cat{C}} = [\cat{C}^{\mathrm{op}}, \cat{Set}]$ and $y : \cat{C} \to \widehat{\cat{C}}$ for the Yoneda embedding, $y(c) = \cat{C}(-, c)$.

The quantifier "for all $f : d \to c$" — at every stage reachable from $c$ — is what separates $\Rightarrow$ from the Boolean $\neg U \cup V$. In particular negation is $(\neg U)(c) = \{ x \mid x \cdot f \notin U(d) \text{ for all } f \}$: "$x$ is never in $U$, at any stage reachable by restriction".

More generally, in every elementary topos each $\mathrm{Sub}(X)$ is a Heyting algebra, the maps $f^*$ are Heyting algebra maps with adjoints $\exists_f \dashv f^* \dashv \forall_f$, and $\Omega$ is an internal Heyting algebra. This is what it means to say that the internal logic of a topos is intuitionistic: higher-order intuitionistic logic is sound for interpretation in any topos, and complete with respect to all toposes (Lambek and Scott 1986). For proofs see Mac Lane and Moerdijk (1992), Chapters IV and VI.

Since every finite distributive lattice is the lattice of down-sets of its poset of join-irreducible elements (Birkhoff's representation theorem), and a finite distributive lattice is automatically a Heyting algebra, every finite Heyting algebra occurs as $\mathrm{Sub}(1)$ of a presheaf topos on a finite poset. Combined with the finite model property of intuitionistic propositional logic, a propositional formula holds for all truth values of all such toposes exactly when it is intuitionistically provable. This is Kripke semantics in topos form: a Kripke frame $(W, \le)$ corresponds to presheaves on $W^{\mathrm{op}}$.

Lawvere's Elementary Theory of the Category of Sets (1964) predates elementary toposes and axiomatises sets structurally: there is no global membership relation, only sets and functions. In the modern topos-theoretic packaging (following Lawvere, Tierney and others around 1970), ETCS says:

Leinster (2014) spells these out as ten informal axioms — associativity of composition, a set with exactly one element, functions determined by their effect on elements, and so on. Some consequences: a well-pointed topos is Boolean and two-valued, so $\Omega \cong 1 + 1 = \{\mathrm{false}, \mathrm{true}\}$; and by Diaconescu's theorem the choice axiom alone already implies excluded middle.

Comparison with ZFC.

Consistency strength. ETCS is equiconsistent with bounded Zermelo set theory with choice — Zermelo set theory with Separation restricted to formulas whose quantifiers are bounded, and without Replacement (Mitchell 1972, Cole 1973, Osius 1974). Since ZFC proves the consistency of bounded Zermelo set theory (for instance $V_{\omega + \omega}$ is a model), ZFC proves the consistency of ETCS; and ETCS cannot prove the consistency of ZFC unless ZFC is inconsistent (ZFC interprets ETCS, so this would contradict Gödel's second incompleteness theorem). So ETCS is strictly weaker than ZFC in consistency strength. Adding a suitable categorical axiom of replacement to ETCS yields a theory of the same strength as ZFC (McLarty 2004; see also Leinster 2014). Much of mathematics outside set theory itself uses neither Replacement nor global membership — a point stressed by Lawvere and by Mac Lane — which is why many working mathematicians find ETCS a faithful description of how sets are actually used; see ZFC for the other side.

We formalise the subobject classifier of the Sierpiński topos from scratch, and cite Mathlib for the general theorem about presheaf categories.

A presheaf on $\{0 < 1\}$ is a pair of types with a restriction map; subpresheaves are pairs of sets closed under restriction (Lemma 2 justifies using them as subobjects):

/-- A **presheaf on the poset `{0 < 1}`**: a type `A₁` of "sections at stage 1", a type `A₀` of
"sections at stage 0", and the restriction map `res : A₁ → A₀` along `0 ≤ 1`. (A functor
`{0 < 1}ᵒᵖ ⥤ Type` is exactly this data: the identities must go to identities, so only `res` is
free.) The category of these is the **Sierpiński topos**, also the arrow category of `Type`. -/
structure Psh where
  /-- Sections at stage `1`. -/
  A1 : Type
  /-- Sections at stage `0`. -/
  A0 : Type
  /-- Restriction from stage `1` to stage `0`. -/
  res : A1 → A0

/-- A **subpresheaf** of `A`: a subset at each stage, closed under restriction. Subobjects of a
presheaf (monomorphisms into it, up to isomorphism) correspond exactly to subpresheaves, because
monomorphisms of presheaves are the pointwise injective natural transformations. -/
@[ext]
structure Sub (A : Psh) where
  /-- The part at stage `1`. -/
  S1 : Set A.A1
  /-- The part at stage `0`. -/
  S0 : Set A.A0
  /-- Restricting a section in the subpresheaf stays in the subpresheaf. -/
  closed : ∀ x, x ∈ S1 → A.res x ∈ S0

A sieve on $1$ is encoded by two propositions — "contains $\mathrm{id}_1$" and "contains $0 \to 1$" — with the first implying the second. This is the sieve description of Theorem 3, and it is faithful even intuitionistically: we never decide whether a proposition is true.

/-- The **subobject classifier** `Ω`. Its stage-`0` sections are the sieves on `0`, i.e. truth
values `Prop`. A sieve on `1` is a downward-closed set of arrows into `1`; it is determined by two
propositions — "contains `id₁`" (true *now*) and "contains `0 ≤ 1`" (true *after restriction*) —
with the first implying the second. Restriction forgets the first. -/
def Omega : Psh where
  A1 := {p : Prop × Prop // p.1 → p.2}
  A0 := Prop
  res p := p.1.2

The characteristic map and the pullback of $\mathrm{true}$ are defined exactly as in the proof of Theorem 3, and the two round trips are the existence and uniqueness halves of the classifier axiom:

/-- The **characteristic map** `χ_S : A ⟶ Ω` of a subpresheaf `S`. A section `x` at stage `1` is
sent to the sieve "`x ∈ S` now, and `res x ∈ S` after restriction"; a section at stage `0` to the
proposition `y ∈ S`. Naturality holds by definition. -/
def chi {A : Psh} (S : Sub A) : Hom A Omega where
  f1 x := ⟨(x ∈ S.S1, A.res x ∈ S.S0), S.closed x⟩
  f0 y := y ∈ S.S0
  comm _ := rfl

/-- The **pullback of `true` along `φ : A ⟶ Ω`**. Pullbacks of presheaves are computed stage by
stage, so this is the subpresheaf of sections that `φ` sends to `true` (the maximal sieve at stage
`1`, the proposition `True` at stage `0`). Closure under restriction comes from naturality of `φ`. -/
def pullbackTrue {A : Psh} (φ : Hom A Omega) : Sub A where
  S1 := {x | φ.f1 x = top1}
  S0 := {y | φ.f0 y}
  closed x hx := by
    have h1 : (φ.f1 x).1.1 := (eq_top1_iff _).1 hx
    have h2 : Omega.res (φ.f1 x) := (φ.f1 x).2 h1
    show φ.f0 (A.res x)
    rw [← φ.comm x]
    exact h2

/-- Pulling `true` back along `χ_S` recovers `S`: the square
`S ↪ A`, `χ_S : A → Ω`, `true : 1 → Ω` is a pullback. -/
theorem pullbackTrue_chi {A : Psh} (S : Sub A) : pullbackTrue (chi S) = S := by
  ext x
  · show (chi S).f1 x = top1 ↔ x ∈ S.S1
    rw [eq_top1_iff]
    rfl
  · rfl

/-- Conversely, every natural map `φ : A ⟶ Ω` is the characteristic map of the subpresheaf it
classifies. At stage `1` the "now" component is recovered by `eq_top1_iff` and the "after
restriction" component by naturality of `φ`. -/
theorem chi_pullbackTrue {A : Psh} (φ : Hom A Omega) : chi (pullbackTrue φ) = φ := by
  apply Hom.ext
  · funext x
    apply Subtype.ext
    show ((φ.f1 x = top1), φ.f0 (A.res x)) = (φ.f1 x).1
    rw [← φ.comm x]
    apply Prod.ext
    · exact propext (eq_top1_iff (φ.f1 x))
    · rfl
  · rfl

/-- **`Ω` classifies subobjects**: subpresheaves of `A` are in bijection with natural maps
`A ⟶ Ω`, via `χ` and pulling back `true`. This is the subobject-classifier axiom for the
Sierpiński topos, in the form "`Sub(A) ≅ Hom(A, Ω)`". -/
def subEquivHom (A : Psh) : Sub A ≃ Hom A Omega where
  toFun := chi
  invFun := pullbackTrue
  left_inv := pullbackTrue_chi
  right_inv := chi_pullbackTrue

Theorem 4 for this topos: Heyting implication is defined with the "now and after restriction" clause, the residuation law is proved, and Mathlib's HeytingAlgebra.ofHImp packages the result as a genuine HeytingAlgebra instance — so all of Mathlib's Heyting-algebra lemmas apply to subpresheaves.

/-- **Heyting implication** of subpresheaves. At stage `0` it is the usual
`{y | y ∈ S → y ∈ T}`. At stage `1`, a section `x` belongs to `S ⇒ T` when the implication holds
*at every stage reachable from `x`*: now, and after restriction. This is the Kripke clause for
implication; the second conjunct is exactly what makes the result closed under restriction. -/
def himp (S T : Sub A) : Sub A where
  S1 := {x | (x ∈ S.S1 → x ∈ T.S1) ∧ (A.res x ∈ S.S0 → A.res x ∈ T.S0)}
  S0 := {y | y ∈ S.S0 → y ∈ T.S0}
  closed _ hx := hx.2

/-- The **residuation law** `U ≤ (S ⇒ T) ↔ U ⊓ S ≤ T`, which makes subpresheaves a Heyting
algebra. The forward direction is modus ponens. For the backward direction at stage `1`, the
"after restriction" clause uses that `U` itself is closed under restriction. -/
theorem le_himp_iff (U S T : Sub A) : U ≤ himp S T ↔ U ⊓ S ≤ T := by
  constructor
  · rintro ⟨h1, h0⟩
    exact ⟨fun x hx => (h1 hx.1).1 hx.2, fun y hy => h0 hy.1 hy.2⟩
  · rintro ⟨h1, h0⟩
    refine ⟨fun x hx => ⟨fun hs => h1 ⟨hx, hs⟩, fun hs => h0 ⟨U.closed x hx, hs⟩⟩,
      fun y hy hs => h0 ⟨hy, hs⟩⟩

/-- **The subobjects of any presheaf on `{0 < 1}` form a Heyting algebra.** Negation is
`¬S = S ⇒ ⊥`. -/
instance instHeytingAlgebra : HeytingAlgebra (Sub A) :=
  HeytingAlgebra.ofHImp himp le_himp_iff

Proposition 5: three truth values, a subobject without complement, and a truth value that is "not not true" without being true.

/-- The terminal presheaf has **exactly three subobjects**: `⊥`, `later` and `⊤` (the case split
on two propositions uses classical logic, as it must: this is a statement *about* the topos, made
in our classical metatheory). -/
theorem sub_one_trichotomy (S : Sub one) : S = ⊥ ∨ S = later ∨ S = ⊤ := by
  by_cases h1 : () ∈ S.S1
  · right; right
    have h0 : () ∈ S.S0 := S.closed () h1
    ext ⟨⟩
    · exact ⟨fun _ => trivial, fun _ => h1⟩
    · exact ⟨fun _ => trivial, fun _ => h0⟩
  · by_cases h0 : () ∈ S.S0
    · right; left
      ext ⟨⟩
      · exact ⟨fun h => (h1 h).elim, fun h => h.elim⟩
      · exact ⟨fun _ => trivial, fun _ => h0⟩
    · left
      ext ⟨⟩
      · exact ⟨fun h => (h1 h).elim, fun h => h.elim⟩
      · exact ⟨fun h => (h0 h).elim, fun h => h.elim⟩

/-- **The Sierpiński topos is not Boolean.** The subobject `later` of `1` has no complement: no
`T` with `later ⊓ T = ⊥` and `later ⊔ T = ⊤`. (Disjointness forces `T` to be empty at stage `0`,
closure then forces it to be empty at stage `1`, and then the union misses stage `1`.) -/
theorem sub_one_not_boolean : ¬ ∃ T : Sub one, later ⊓ T = ⊥ ∧ later ⊔ T = ⊤ := by
  rintro ⟨T, hinf, hsup⟩
  have hT0 : () ∉ T.S0 := fun h => by
    have : () ∈ (later ⊓ T).S0 := ⟨trivial, h⟩
    rw [hinf] at this
    exact this
  have hT1 : () ∉ T.S1 := fun h => hT0 (T.closed () h)
  have : () ∈ (later ⊔ T).S1 := by
    rw [hsup]
    trivial
  rcases this with h | h
  · exact h
  · exact hT1 h

/-- Yet `later` is "not not true": its double negation is `⊤`, while `later ≠ ⊤`. So
`¬¬p → p` fails too — a hallmark of intuitionistic logic. -/
theorem not_not_later : laterᶜᶜ = ⊤ ∧ later ≠ ⊤ := by
  refine ⟨?_, fun h => ?_⟩
  · apply le_antisymm le_top
    rw [le_compl_iff_disjoint_right, disjoint_iff]
    -- `laterᶜ` is empty at stage `0` (since `later` is full there) and hence at stage `1`.
    ext ⟨⟩
    · exact ⟨fun hx => (hx.2.2 trivial).elim, fun hx => hx.elim⟩
    · exact ⟨fun hx => hx.2 trivial, fun hx => hx.elim⟩
  · have : () ∈ (⊤ : Sub one).S1 := trivial
    rw [← h] at this
    exact this

The axiom lists shown with each declaration are instructive: the classifier bijection and not_not_later use only propext and Quot.sound, not Classical.choice, while the trichotomy — a statement about the topos, made in our classical metatheory — needs a classical case split on two propositions and so depends on Classical.choice.

Finally, Mathlib proves the general Theorem 3: every presheaf category on a small category has finite limits, a subobject classifier (built, as in our proof, from the presheaf of sieves) and internal homs for the pointwise product.

/-- **Every presheaf category on a small category is an elementary topos**: it has finite limits,
a subobject classifier (Mathlib's `HasSubobjectClassifier` instance from
`Mathlib.CategoryTheory.Topos.Sheaf`, whose `Ω` is the presheaf of sieves), and internal homs
(`MonoidalClosed`, from `Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes`) for the pointwise
product — which is the categorical product, see `presheaf_tensor_eq_prod`. All three are
instances found by `inferInstance`. -/
theorem presheaf_category_is_topos (C : Type u) [SmallCategory C] :
    HasFiniteLimits (Cᵒᵖ ⥤ Type u) ∧ HasSubobjectClassifier (Cᵒᵖ ⥤ Type u) ∧
      Nonempty (MonoidalClosed (Cᵒᵖ ⥤ Type u)) :=
  ⟨inferInstance, inferInstance, ⟨inferInstance⟩⟩

The closed structure is with respect to Mathlib's monoidal structure on functor categories, which is the pointwise cartesian product — so this is cartesian closure:

/-- The monoidal product used by the closed structure above is the pointwise cartesian product:
`(F ⊗ G)(c) = F(c) × G(c)`, by definition of Mathlib's monoidal structure on functor categories.
Mathlib also makes it a `CartesianMonoidalCategory` (chosen finite products), so `MonoidalClosed`
here is cartesian closedness. -/
theorem presheaf_tensor_eq_prod (C : Type u) [SmallCategory C] (F G : Cᵒᵖ ⥤ Type u) (c : Cᵒᵖ) :
    (F ⊗ G).obj c = (F.obj c × G.obj c) :=
  rfl

What is and is not formalised. Formalised: the Sierpiński classifier (independently), the Heyting algebra of subpresheaves on $\{0 < 1\}$ and its failure to be Boolean (independently), and Theorem 3 in general (from Mathlib). Not formalised here: our concrete Psh is not proved equivalent to Mathlib's functor category on $\{0 < 1\}^{\mathrm{op}}$; Theorem 4 for arbitrary presheaf categories; the Heyting algebra of subobjects in an arbitrary topos and the internal language (Mathlib has the lattice of subobjects in a general category, Subobject B, but we found no Heyting structure or internal language for toposes); and ETCS.

For presheaves on a finite poset everything is finite and can be computed: the sieves $\Omega(p)$, the subpresheaves of a small presheaf, all natural maps into $\Omega$, and the Heyting operations on truth values. The experiment checks the classifier bijection of Theorem 3 for every presheaf on $\{0 < 1\}$ with at most four sections at stage 1 and three at stage 0, and finds which posets give Boolean truth values.

"""The subobject classifier of a presheaf topos, computed exactly.

For presheaves on a finite poset P, the classifier Omega has Omega(p) = the
sieves on p (down-closed subsets of the principal down-set of p), and the
global truth values are the down-sets of P. This experiment

1. counts sieves on a chain (|Omega(k)| = k + 2) and on other small posets;
2. checks, for every presheaf A on {0 < 1} with |A1| <= 4 and |A0| <= 3,
   that A has exactly as many subpresheaves as natural maps A -> Omega, and
   that the characteristic map chi is a bijection between them;
3. computes the Heyting algebra of truth values and finds where excluded
   middle fails.

Evidence: exact computation and exhaustive checks of finitely many cases.
"""

import itertools
import textwrap

def down_sets(elements, leq):
    """All down-closed subsets of the finite poset (elements, leq)."""
    found = []
    for r in range(len(elements) + 1):
        for combo in itertools.combinations(elements, r):
            s = frozenset(combo)
            if all(q in s for p in s for q in elements if leq(q, p)):
                found.append(s)
    return found

def sieves_on(p, elements, leq):
    """Sieves on p: down-closed subsets of {q | q <= p}."""
    below = [q for q in elements if leq(q, p)]
    return down_sets(below, leq)

def chain(n):
    """The chain 0 < 1 < ... < n-1 as (elements, leq)."""
    return list(range(n)), lambda a, b: a <= b

def heyting_implies(u, v, opens):
    """Largest member w of `opens` with w & u <= v (the Heyting implication)."""
    best = frozenset()
    for w in opens:
        if w & u <= v:
            best = best | w
    assert best in opens
    return best

def excluded_middle_failures(elements, leq):
    """Down-sets u with u | (not u) != everything, where not u = u => empty."""
    opens = down_sets(elements, leq)
    top = frozenset(elements)
    return [u for u in opens
            if u | heyting_implies(u, frozenset(), opens) != top]

OMEGA1 = [(a, b) for a in (False, True) for b in (False, True) if a <= b]

def subpresheaves(a1, a0, res):
    """Pairs (S1, S0) of subsets with res(S1) inside S0."""
    subs = []
    for r0 in range(a0 + 1):
        for s0 in itertools.combinations(range(a0), r0):
            for r1 in range(a1 + 1):
                for s1 in itertools.combinations(range(a1), r1):
                    if all(res[x] in s0 for x in s1):
                        subs.append((frozenset(s1), frozenset(s0)))
    return subs

def natural_maps(a1, a0, res):
    """Natural maps A -> Omega: (f1, f0) with f1(x)[1] == f0(res x)."""
    maps = []
    for f0 in itertools.product((False, True), repeat=a0):
        for f1 in itertools.product(OMEGA1, repeat=a1):
            if all(f1[x][1] == f0[res[x]] for x in range(a1)):
                maps.append((f1, f0))
    return maps

def chi(sub, a1, a0, res):
    """Characteristic map of a subpresheaf (S1, S0)."""
    s1, s0 = sub
    f1 = tuple((x in s1, res[x] in s0) for x in range(a1))
    return f1, tuple(y in s0 for y in range(a0))

def check_classifier(max1=4, max0=3):
    """Return (presheaves checked, failures) for the bijection Sub = Hom."""
    checked, failures = 0, []
    for a1 in range(max1 + 1):
        for a0 in range(max0 + 1):
            for res in itertools.product(range(a0), repeat=a1):
                subs = subpresheaves(a1, a0, res)
                maps = set(natural_maps(a1, a0, res))
                images = {chi(s, a1, a0, res) for s in subs}
                if len(images) != len(subs) or images != maps:
                    failures.append((a1, a0, res))
                checked += 1
    return checked, failures

POSETS = {
    "{0<1}": chain(2),
    "chain of 3": chain(3),
    "0 < 2 > 1": ([0, 1, 2], lambda a, b: a == b or b == 2),
    "discrete 3": ([0, 1, 2], lambda a, b: a == b),
}

def main():
    elems, leq = chain(5)
    sizes = [len(sieves_on(k, elems, leq)) for k in elems]
    print(f"Chain 0<1<2<3<4: |Omega(k)| = {sizes} (k + 2 each)")
    print()
    checked, failures = check_classifier()
    print("Presheaves A on {0<1} with |A1| <= 4, |A0| <= 3 (all restrictions):")
    print(f"  {checked} presheaves; chi : Sub(A) -> Hom(A, Omega) failed to be a")
    print(f"  bijection in {len(failures)} of them.")
    a1, a0, res = 3, 2, (0, 0, 1)
    n_sub = len(subpresheaves(a1, a0, res))
    print(f"  Example res = {res}: {n_sub} subpresheaves = (1 + 2^2)(1 + 2^1).")
    print()
    print("Global truth values = down-sets of P:")
    for name, (el, le) in POSETS.items():
        opens = down_sets(el, le)
        bad = excluded_middle_failures(el, le)
        status = "Boolean" if not bad else f"not Boolean ({len(bad)} fail LEM)"
        print(f"  {name:<12} {len(opens):>2} truth values, {status}")
    el, le = chain(2)
    opens = down_sets(el, le)
    half = frozenset({0})
    neg = heyting_implies(half, frozenset(), opens)
    negneg = heyting_implies(neg, frozenset(), opens)
    print("In {0<1}: u = {0} ('true only after restriction'):")
    print(f"  not u = {sorted(neg)}, not not u = {sorted(negneg)},"
          f" u or not u = {sorted(half | neg)}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact computations and an exhaustive check of "
        f"{checked} small presheaves. They illustrate, but do not prove, the "
        "theorems that Omega classifies subobjects in every presheaf topos "
        "and that its truth values form a Heyting algebra; those are proved "
        "in the lesson, and the {0<1} case is also checked in Lean.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Two things to notice. The number of subpresheaves of $A$ — and hence, by the bijection, of natural maps $A \to \Omega$ — is $\prod_{y \in A_0} (1 + 2^{k_y})$, where $k_y$ is the size of the fibre of $\mathrm{res}$ over $y$ (see the exercises). And among the posets tried only the discrete one gives a Boolean algebra of truth values. This is always so: the only possible complement of a down-set $D$ is $P \setminus D$, and if $a < b$ then $P \setminus {\downarrow} a$ contains $b$ but not $a$, so it is not a down-set and ${\downarrow} a$ has no complement. The computation is exhaustive only for the listed finite cases; the theorems above are what cover all presheaves.

The truth-table explorer below computes classical (two-valued) truth tables — the logic of the Boolean topos $\cat{Set}$. Both formulas are classical tautologies, so their columns agree.

In the Sierpiński topos the truth values form the chain $0 < \tfrac12 < 1$, where $a \Rightarrow b = 1$ if $a \le b$ and $a \Rightarrow b = b$ otherwise, and $\neg a = a \Rightarrow 0$:

Try other formulas in the explorer and then evaluate them by hand on the three-element chain. Peirce's law $((p \to q) \to p) \to p$ is a classical tautology that fails at $p = \tfrac12$, $q = 0$. The weak De Morgan law $\neg(p \wedge q) \to \neg p \vee \neg q$ survives on the chain, but fails for presheaves on the poset $0 < 2 > 1$ (take $p$, $q$ to be the down-sets $\{0\}$ and $\{1\}$). In the other direction, a formula that is not a classical tautology already fails at the truth values $0$ and $1$ of any non-degenerate topos.