PeanoSurface

formal source

  69namespace ArithmeticOf
  70
  71/-- Peano surface of a forced arithmetic object. -/
  72structure PeanoSurface {R : LogicRealization} (A : ArithmeticOf R) : Prop where
  73  zero_ne_step : ∀ x : A.peano.carrier, A.peano.zero ≠ A.peano.step x
  74  step_injective : Function.Injective A.peano.step
  75  induction :
  76    ∀ P : A.peano.carrier → Prop,
  77      P A.peano.zero →
  78      (∀ n, P n → P (A.peano.step n)) →
  79      ∀ n, P n
  80
  81/-! ## LogicNat as the canonical initial Peano object -/
  82
  83/-- The Peano object carried by `LogicNat`. -/
  84def logicNatPeano : PeanoObject where
  85  carrier := LogicNat
  86  zero := LogicNat.zero
  87  step := LogicNat.succ
  88
  89/-- Fold from `LogicNat` into an arbitrary Peano object. -/
  90def logicNatFold (B : PeanoObject) : LogicNat → B.carrier
  91  | LogicNat.identity => B.zero
  92  | LogicNat.step n => B.step (logicNatFold B n)
  93
  94/-- Lift from `LogicNat` to any Peano object by primitive recursion. -/
  95def logicNatLift (B : PeanoObject) : PeanoObject.Hom logicNatPeano B where
  96  toFun := logicNatFold B
  97  map_zero := rfl
  98  map_step := by
  99    intro x
 100    rfl
 101
 102private theorem logicNatLift_unique_fun (B : PeanoObject)