def
definition
terminalReality
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.RealityTerminalCategory on GitHub at line 77.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
74/-- The terminal reality certificate is the certificate of the minimal Bool
75carrier. Every other distinguished carrier has a unique terminal arrow to the
76same proposition-shaped reality object. -/
77def terminalReality : TerminalArrow boolObject :=
78 terminalArrow_exists boolObject
79
80/-- Any distinguished carrier has the same forced reality content, in the
81categorical/propositional sense: there is a unique morphism from it to the
82terminal certificate. -/
83theorem every_distinguished_carrier_maps_uniquely_to_reality
84 (A : DistinguishedCarrier) :
85 ∃! f : TerminalArrow A, True :=
86 terminalArrow_unique_exists A
87
88/-! ## Certificate -/
89
90structure RealityTerminalCert where
91 object : DistinguishedCarrier
92 terminal : TerminalArrow object
93 universal :
94 ∀ A : DistinguishedCarrier, ∃! f : TerminalArrow A, True
95
96def realityTerminalCert : RealityTerminalCert where
97 object := boolObject
98 terminal := terminalReality
99 universal := every_distinguished_carrier_maps_uniquely_to_reality
100
101end RealityTerminalCategory
102end Foundation
103end IndisputableMonolith