canonicity
plain-language theorem explainer
Every closed term of the two-element type is either false or true: the type has exactly two inhabitants. Recognition Science cites this as type theory's canonicity witness for the primitive distinction δ. Anyone packaging the type-theory foundation parse, or proving the three foundations own their distinctions, depends on it. The proof is a pure constructor case split.
Claim. Let $\mathbb{2}$ be the canonical two-element type (Martin-Löf / CIC, here identified with $\mathsf{Bool}$). For every closed $b:\mathbb{2}$, either $b=\mathsf{false}$ or $b=\mathsf{true}$. Equivalently, $\mathbb{2}$ has exactly two inhabitants, the two canonical constructors.
background
In the Primitive Recognition Calculus type-theory parse, the two-element type $\mathbb{2}$ is taken as Lean's Bool, with closed constructors false and true. The module reads type theory as one of three classical foundations (with set theory and topos/category theory) and asks whether each foundation supplies its own non-degenerate distinction mechanism for the δ core.
Canonicity is the type-theoretic half of that mechanism: every closed term of $\mathbb{2}$ is definitionally one of the two constructors. The companion fact is no-confusion (the constructors are distinct). Together they say the foundation can tell its two primitives apart without external data.
Upstream, the parse sits beside other "canonical" objects in the monolith (canonical arithmetic, canonical dyadic protocols, canonical completed traces). Those are different canonicity notions; here the word means only inhabitant-canonicity for $\mathbb{2}$.
proof idea
Term-mode proof by cases on the Boolean $b$. The false branch discharges the left disjunct by reflexivity; the true branch discharges the right disjunct by reflexivity. No lemmas are invoked: the recursor for the inductive two-element type is the entire argument.
why it matters
This is type theory's own distinction act in the three-foundations comparison. Downstream, three_foundations_own_distinction packages it with set-theoretic extensionality and topos subobject classification as the three foundations' native ways of separating primitives, each yielding δ. The packaged theorem type_theory_realizes_delta conjoins canonicity, no-confusion, and a nonempty embedding of the δ core into the type-theory system; non-degeneracy of that system then follows.
Further up the stack, distinction-forcing uniqueness and the canonical-forcing certificate use the same pattern: maps and equivalences between forced arithmetics are determined by distinction data alone, with no representational freedom. In the Recognition forcing chain this is the type-theoretic instance of "the distinction is forced, not chosen."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.