classifies_top
plain-language theorem explainer
The full subobject of the terminal object is classified by the truth value ⊤. Category theorists and anyone tracking the PRC parse of foundations would cite this as the positive half of subobject classification. The proof is definitional: the classifier evaluates the constant-true predicate at the unique point of the terminal object.
Claim. Under the subobject classification equivalence that sends a predicate $f : 1 \to \mathrm{Prop}$ to the truth value $f(\ast) \in \Omega$, the constant-true predicate (the whole terminal object) is sent to $\top$.
background
In the Primitive Recognition Calculus category-theory parse, the terminal object is the unit type $1$, and its subobjects are predicates $1 \to \mathrm{Prop}$. The two-point classifier $\Omega$ is identified with $\mathrm{Prop}$ itself (global truth values).
The map subobjectClassification is the standard characteristic-morphism bijection: a subobject $f$ is sent to the single truth value $f(\ast)$. Its inverse constantly re-embeds a truth value as a predicate on $1$. The doc-comment states the intent: subobjects of the terminal object are in bijection with global points of $\Omega$.
This lemma records the positive endpoint of that bijection: the maximal subobject (everything) has characteristic value $\top$.
proof idea
One-line definitional proof by rfl. Unfolding the forward map of the equivalence gives evaluation at the unique inhabitant of Unit, and (fun _ => True) () is definitionally True. No lemmas are invoked.
why it matters
Feeds directly into category_theory_realizes_delta, which packages the faithful parse: classifier of the full subobject is $\top$, of the empty subobject is $\bot$, the two truth values are distinct, and the topos system embeds the $\delta$ core. Also appears as the category-theory conjunct of three_foundations_own_distinction, where set-theoretic extensionality, type-theoretic canonicity, and categorical subobject classification are each shown to own the primitive distinction mechanism.
In the Recognition Science foundation layer this is the categorical half of telling two primitives apart: $\top$ versus $\bot$ on the classifier, parallel to the $\delta$ distinction that the forcing chain later specializes. It is elementary topos structure, not a deep forcing step, but it closes the parse that category theory realizes $\delta$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.