terminalReality
plain-language theorem explainer
terminalReality supplies the terminal arrow from the minimal Boolean carrier into the reality certificate. Researchers formalizing the categorical master theorem cite it to witness that every distinguished carrier maps uniquely to the same proposition-shaped reality object. The definition is a direct one-line application of the existence lemma for terminal arrows.
Claim. Let $B$ be the distinguished carrier given by the Boolean type with its two distinct elements. There exists a morphism from $B$ to the terminal reality object, which is the proposition that $B$ admits a reality certificate.
background
This module records the universal property that every distinguished carrier maps uniquely to a single reality certificate. A distinguished carrier consists of an inhabited type together with a named distinction between two elements. TerminalArrow from such a carrier is defined to be exactly the proof that the carrier possesses a reality certificate.
proof idea
This is a one-line wrapper that applies the terminalArrow_exists lemma directly to boolObject.
why it matters
It supplies the concrete terminal arrow required to build the RealityTerminalCert record, which packages the object, the terminal map, and the universal property. This completes the terminal-object reading of the master theorem, showing that forced reality content is independent of the choice of distinguished carrier. The construction relies on reality_from_one_distinction for existence and proof irrelevance for uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.