terminalArrow_unique
plain-language theorem explainer
Any two terminal arrows from a distinguished carrier are equal because TerminalArrow A is a proposition. Researchers assembling the categorical master theorem would cite this when closing the uniqueness half of the terminal-object property. The proof is a one-line term application of Subsingleton.elim on the subsingleton type.
Claim. Let $A$ be a distinguished carrier (a type equipped with two distinct points). If $f$ and $g$ are proofs that the reality certificate exists for the carrier of $A$, then $f = g$.
background
The RealityTerminalCategory module encodes the terminal-object reading of the master theorem. Objects are distinguished carriers: structures containing a carrier type, a base point, a witness point, and a proof that the points differ. A terminal arrow from such an object is defined as the proposition RealityCertificate on the carrier type, making the arrow type itself a Prop.
proof idea
The proof is the term Subsingleton.elim f g. TerminalArrow A is literally a Prop (RealityCertificate A.Carrier), so the type of arrows is a subsingleton and any two elements coincide by the standard Lean elimination rule for proof-irrelevant propositions.
why it matters
This supplies the uniqueness direction that terminalArrow_unique_exists packages into the full existence-and-uniqueness statement. It realizes the module's stated terminal-object formulation: every distinguished carrier maps uniquely to the forced reality certificate. The result sits inside the foundation layer that supports the forcing chain by guaranteeing a single terminal reality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.