toposSystem_embeds_delta
plain-language theorem explainer
The topos-of-sets foundation, parsed as a formal system with tokens the global points of Ω, admits a Primitive Recognition Calculus embedding that preserves endpoint distinction and finite trace extension. Anyone checking that category theory realizes the δ-core (alongside set and type theory) cites this. The proof is a one-line wrapper: expressiveness of the topos system (⊤ ≠ ⊥) feeds the general embedding theorem for expressive formal systems.
Claim. There exists a PRC embedding into the topos formal system: maps send the two primitive endpoints to $\top,\bot\in\Omega$, preserve the endpoint distinction ($\top\neq\bot$), and preserve finite trace extension under the derivation-length order on expressions.
background
Primitive Recognition Calculus (PRC) isolates a minimal δ-core: two distinguished endpoints and finite traces that extend. A formal system is any token/expression interface with a discrimination relation and an expression-extension order. A PRC embedding into such a system is a pair of maps (endpoints to tokens, traces to expressions) that preserve distinction of the two endpoints and monotonicity of trace extension.
Here the formal system is the category-theoretic parse: tokens are global points of the subobject classifier Ω (truth values), discrimination is inequality of those points, the endpoints are ⊤ and ⊥, and expressions are ordered by derivation length. Expressiveness of this system is exactly ⊤ ≠ ⊥.
Upstream, any expressive formal system admits a PRC embedding (the general embedding-target theorem constructs it from the expressive witness). The local module only has to supply that witness for the topos parse.
proof idea
One-line wrapper. Apply the general theorem that every expressive formal system admits a PRC embedding, instantiating the system by the topos parse and the expressiveness hypothesis by the already-proved fact that ⊤ ≠ ⊥ in Ω. No further case analysis or construction is performed at this site.
why it matters
This is the category-theory leg of the claim that the three named foundations each realize the δ-core. It is packaged into the faithful-parse theorem (subobject classification of the constant-true and constant-false predicates, non-degeneracy of Ω, and existence of the embedding) and into the non-degeneracy corollary for the topos system. Downstream it also feeds the three-foundations conjunction that set theory, type theory, and category theory each admit a PRC embedding. In the Recognition framework this anchors the claim that the δ distinction is not an artifact of one foundation's syntax but is realized by the standard categorical foundation via its two-point classifier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.