IndisputableMonolith.Foundation.RealityTerminalCategory

   1import IndisputableMonolith.Foundation.RealityFromDistinction
   2
   3/-!
   4# Terminal Reality Certificate
   5
   6This module repairs the categorical form of the master theorem.
   7
   8The point is not to build the full Mathlib category-theory interface. The
   9point is to record the universal property that matters here:
  10
  11* objects are inhabited carriers with a named distinction;
  12* a morphism from such an object to the terminal reality certificate is
  13  precisely a proof that its `RealityCertificate` exists;
  14* such a morphism exists for every object by `reality_from_one_distinction`;
  15* such a morphism is unique by proof irrelevance, since `RealityCertificate`
  16  is a proposition.
  17
  18This is the terminal-object reading of the master theorem: any distinguished
  19carrier maps uniquely into the same forced reality certificate.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace RealityTerminalCategory
  25
  26open RealityFromDistinction
  27
  28/-! ## Objects -/
  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 :=
  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
  72/-! ## The terminal reality object -/
  73
  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
 104