subobjectClassification
plain-language theorem explainer
Subobjects of the terminal object, written as predicates on the unit type, stand in canonical bijection with global points of the subobject classifier Ω (identified with Prop). Anyone citing the category-theoretic parse of the δ distinction uses this equivalence. The map is evaluation at the unique point, inverted by constant predicates; the two inverse laws are immediate from funext and unit elimination.
Claim. There is a canonical equivalence $(1 \to \Omega) \simeq \Omega$ between predicates on the terminal object $1$ and global elements of the subobject classifier $\Omega$, where $\Omega$ is the type of propositions. A predicate $f : 1 \to \mathrm{Prop}$ is sent to the truth value $f(\ast)$; a truth value $p$ is sent to the constant predicate with value $p$. These maps are mutually inverse.
background
In the topos of sets the subobject classifier $\Omega$ is the type of truth values (here abbreviated as Prop). Its two global points are truth and falsity. Subobjects of an object $X$ are classified by characteristic maps $X \to \Omega$; specializing to the terminal object $1$ (the unit type), those characteristic maps are exactly predicates $1 \to \mathrm{Prop}$, and global points of $\Omega$ are just elements of $\mathrm{Prop}$.
This module is the category-theory parse of Primitive Recognition Calculus: it packages the elementary topos structure of sets so that the $\delta$ distinction (two primitives told apart) can be read off subobject classification rather than from set membership or type canonicity. The local setting is therefore the standard Set-topos facts needed for that parse, not a general topos theory development.
proof idea
The declaration is an explicit equivalence construction, not a tactic proof of a proposition. Forward map: evaluate the predicate at the unique inhabitant of the unit type. Inverse map: send a proposition $p$ to the constant predicate with value $p$. Left inverse: funext over the unit type, then case-split the unique constructor and reduce by reflexivity. Right inverse: definitional, by reflexivity on the constant predicate.
why it matters
This equivalence is the concrete carrier of "category theory owns distinction" in the foundations parse. Downstream, the two specializations that the whole terminal object classifies as $\top$ and the empty subobject classifies as $\bot$ are one-line applications of it; non-degeneracy $\top \neq \bot$ then sits beside them. Those three facts, plus an embedding of the $\delta$ core into the packaged topos system, assemble into the faithful parse theorem that the topos of sets realizes $\delta$.
Further downstream, the three-foundations theorem cites the top-classification instance as category theory's own distinction mechanism, parallel to set-theoretic extensionality and type-theoretic canonicity. In the Recognition forcing chain this is foundation-level scaffolding for the $\delta$ dichotomy, not yet a physics step (T5--T8, RCL, mass ladder); it certifies that the categorical parse is non-vacuous before those layers attach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.