IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCategoryTheoryParse

   1/-
   2  PrimitiveRecognitionCalculus/PRCCategoryTheoryParse.lean
   3
   4  Item 4 of the δ frontier, third corpus parse: a category-theoretic foundation
   5  (the topos of sets, via its subobject classifier), faithfully encoded, shown to
   6  contain δ.
   7
   8  In a categorical / topos-theoretic foundation (ETCS, an elementary topos), the
   9  primitive distinction lives in the SUBOBJECT CLASSIFIER Ω: the truth-value object
  10  carrying two global points ⊤ and ⊥ that classify, respectively, the whole
  11  terminal object and the empty subobject. A topos is non-degenerate exactly when
  12  ⊤ ≠ ⊥ (when 0 ≇ 1).
  13
  14  For the topos of sets, the subobject classifier is the type of truth values, Ω =
  15  `Prop`. We encode this directly:
  16
  17  * SUBOBJECT CLASSIFICATION (`subobjectClassification`): subobjects of the terminal
  18    object 1 (= `Unit`) are in bijection with global points of Ω. The bijection
  19    sends a subobject to its characteristic truth value.
  20  * The two truth values classify the two extreme subobjects (`classifies_top`,
  21    `classifies_bot`): ⊤ ↔ all of 1, ⊥ ↔ the empty subobject.
  22  * NON-DEGENERACY (`top_ne_bot`): ⊤ ≠ ⊥, so Set is a non-degenerate topos.
  23
  24  `toposSystem` parses this foundation into the `FormalSystem` interface: tokens are
  25  global points of Ω (truth values), the discrimination relation is their
  26  inequality, the endpoints are ⊤ and ⊥. It is `Expressive`, so it realizes the δ
  27  core, and it falls on the δ side of the distinction dichotomy.
  28
  29  HONEST BOUNDARY. We use the subobject classifier of the concrete topos Set
  30  (Ω = Prop), which is the genuine categorical truth-value object for that topos. We
  31  do not develop the general elementary-topos axioms in `CategoryTheory` and run the
  32  parse over an arbitrary topos; the δ core needs only the two-point classifier,
  33  which every non-degenerate topos has. A degenerate topos has ⊤ = ⊥ and is exactly
  34  the one the dichotomy classifies as distinction-free.
  35
  36  No project-local axioms. No sorry.
  37-/
  38
  39import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy
  40
  41namespace IndisputableMonolith
  42namespace Foundation
  43namespace PrimitiveRecognitionCalculus
  44namespace CategoryTheoryParse
  45
  46open FormalSystem
  47
  48/-- The subobject classifier Ω of the topos of sets: the type of truth values. Its
  49two global points are truth and falsity. -/
  50abbrev Omega := Prop
  51
  52/-- **Subobject classification for the terminal object.** Subobjects of the
  53terminal object 1 (= `Unit`), presented as predicates `Unit → Prop`, are in
  54bijection with global points of the classifier Ω. The map sends a subobject to its
  55characteristic truth value. -/
  56def subobjectClassification : (Unit → Prop) ≃ Omega where
  57  toFun f := f ()
  58  invFun p := fun _ => p
  59  left_inv f := by funext u; cases u; rfl
  60  right_inv _ := rfl
  61
  62/-- ⊤ classifies the whole terminal object. -/
  63theorem classifies_top : subobjectClassification (fun _ => True) = True := rfl
  64
  65/-- ⊥ classifies the empty subobject. -/
  66theorem classifies_bot : subobjectClassification (fun _ => False) = False := rfl
  67
  68/-- **Non-degeneracy.** The two truth values are distinct: ⊤ ≠ ⊥. A topos with
  69⊤ = ⊥ is degenerate (the terminal category, where 0 ≅ 1). -/
  70theorem top_ne_bot : (True : Omega) ≠ False := by
  71  intro h
  72  rw [eq_iff_iff] at h
  73  exact h.mp trivial
  74
  75/-- A category-theoretic foundation parsed into the `FormalSystem` interface. Tokens
  76are global points of Ω (truth values); the discrimination relation is their
  77inequality; the endpoints are ⊤ and ⊥; the expression order is the
  78derivation-length order. -/
  79def toposSystem : FormalSystem where
  80  Token := Omega
  81  Expr := ℕ
  82  distinguishes := fun a b => a ≠ b
  83  exprExtends := fun m n => m ≤ n
  84  endpointToken := fun e =>
  85    match e.side with
  86    | Side.left => True
  87    | Side.right => False
  88  traceExpr := Trace.length
  89  traceExpr_extends := fun h => InevitabilityInstances.length_le_of_extends h
  90
  91theorem toposSystem_expressive : toposSystem.Expressive := by
  92  show (True : Omega) ≠ False
  93  exact top_ne_bot
  94
  95/-- **The categorical foundation contains the δ core.** -/
  96theorem toposSystem_embeds_delta : Nonempty (PRCEmbeddingInto toposSystem) :=
  97  FormalSystemEmbeddingTarget_proved toposSystem toposSystem_expressive
  98
  99theorem toposSystem_exprReflexive : DistinctionDichotomy.ExprReflexive toposSystem :=
 100  fun n => Nat.le_refl n
 101
 102theorem toposSystem_not_degenerate : ¬ DistinctionDichotomy.Degenerate toposSystem :=
 103  DistinctionDichotomy.not_degenerate_of_realizesDelta toposSystem toposSystem_embeds_delta
 104
 105/-- **The faithful parse, packaged.** The topos of sets has a two-point subobject
 106classifier Ω = Prop classifying the subobjects of the terminal object, its two
 107truth values are distinct (non-degeneracy), and the foundation realizes the δ
 108core. -/
 109theorem category_theory_realizes_delta :
 110    subobjectClassification (fun _ => True) = True
 111      ∧ subobjectClassification (fun _ => False) = False
 112      ∧ ((True : Omega) ≠ False)
 113      ∧ Nonempty (PRCEmbeddingInto toposSystem) :=
 114  ⟨classifies_top, classifies_bot, top_ne_bot, toposSystem_embeds_delta⟩
 115
 116end CategoryTheoryParse
 117end PrimitiveRecognitionCalculus
 118end Foundation
 119end IndisputableMonolith
 120