logicNatFold

formal source

  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)
 103    (f : PeanoObject.Hom logicNatPeano B) :
 104    f.toFun = (logicNatLift B).toFun := by
 105  funext n
 106  induction n with
 107  | identity =>
 108      exact f.map_zero
 109  | step n ih =>
 110      calc
 111        f.toFun (LogicNat.step n) = B.step (f.toFun n) := f.map_step n
 112        _ = B.step ((logicNatLift B).toFun n) := by rw [ih]
 113        _ = (logicNatLift B).toFun (LogicNat.step n) := rfl
 114
 115/-- `LogicNat` is initial among Peano objects. -/
 116def logicNat_initial : PeanoObject.IsInitial logicNatPeano where
 117  lift := logicNatLift
 118  uniq := by
 119    intro B f g
 120    rw [logicNatLift_unique_fun B f, logicNatLift_unique_fun B g]