def
definition
boolObject
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.RealityTerminalCategory on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
38instance (A : DistinguishedCarrier) : Nonempty A.Carrier := ⟨A.base⟩
39
40/-- The minimal distinguished carrier: `Bool`, with `false ≠ true`. -/
41def boolObject : DistinguishedCarrier where
42 Carrier := Bool
43 base := false
44 witness := true
45 distinct := SelfBootstrap.bool_distinguishable
46
47/-! ## Terminal arrows -/
48
49/-- A morphism from a distinguished carrier to the terminal reality object is
50just the proof that the carrier's reality certificate exists. -/
51def TerminalArrow (A : DistinguishedCarrier) : Prop :=
52 RealityCertificate A.Carrier
53
54/-- Every distinguished carrier has a terminal arrow. -/
55theorem terminalArrow_exists (A : DistinguishedCarrier) :
56 TerminalArrow A :=
57 reality_from_one_distinction A.Carrier ⟨A.base, A.witness, A.distinct⟩
58
59/-- The terminal arrow is unique. Since `TerminalArrow A` is a proposition,
60this is proof irrelevance. -/
61theorem terminalArrow_unique (A : DistinguishedCarrier)
62 (f g : TerminalArrow A) : f = g :=
63 Subsingleton.elim f g
64
65/-- Terminality packaged in the usual existence-and-uniqueness shape. -/
66theorem terminalArrow_unique_exists (A : DistinguishedCarrier) :
67 ∃! f : TerminalArrow A, True := by
68 refine ⟨terminalArrow_exists A, trivial, ?_⟩
69 intro g _
70 exact terminalArrow_unique A g (terminalArrow_exists A)
71