`IndisputableMonolith.Foundation.UniversalForcing.CategoricalRealization`

IndisputableMonolith/Foundation/UniversalForcing/CategoricalRealization.lean · 31 lines · 2 declarations

Explainer status: pending

   1import IndisputableMonolith.Foundation.CategoricalLogicRealization
   2
   3/-!
   4  CategoricalRealization.lean
   5
   6  Re-export of the canonical categorical/Lawvere-style realization under the
   7  `Foundation.UniversalForcing` module tree.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace UniversalForcing
  13namespace CategoricalRealization
  14
  15open CategoricalLogicRealization
  16
  17/-- Canonical categorical realization via the `LogicNat` Peano object. -/
  18def categoricalRealization : LogicRealization :=
  19  canonicalCategoricalRealization
  20
  21/-- Categorical realization carries the universal forced arithmetic. -/
  22noncomputable def categorical_arith_equiv_logicNat :
  23    (arithmeticOf categoricalRealization).peano.carrier
  24      ≃ ArithmeticFromLogic.LogicNat :=
  25  categoricalRealization.orbitEquivLogicNat
  26
  27end CategoricalRealization
  28end UniversalForcing
  29end Foundation
  30end IndisputableMonolith
  31

source mirrored from github.com/jonwashburn/shape-of-logic