`DistinguishedCarrier`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.RealityTerminalCategory
domain: Foundation
line: 32 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.RealityTerminalCategory on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  29
  30/-- An object of the distinguished-carrier category: a carrier with two
  31named distinguishable points. -/
  32structure DistinguishedCarrier where
  33  Carrier : Type
  34  base : Carrier
  35  witness : Carrier
  36  distinct : base ≠ witness
  37
  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 :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.