def
definition
categoricalRealization
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.CategoricalRealization on GitHub at line 18.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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