logicNat_initial

formal source

 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]
 121
 122/-- The Peano object extracted from a realization's own orbit. -/
 123def realizationPeano (R : LogicRealization) : PeanoObject where
 124  carrier := R.Orbit
 125  zero := R.orbitZero
 126  step := R.orbitStep
 127
 128/-- Fold from a realization orbit into any Peano object, through the
 129realization's certified equivalence with `LogicNat`. -/
 130def realizationFold (R : LogicRealization) (B : PeanoObject) : R.Orbit → B.carrier :=
 131  fun n => (logicNatLift B).toFun (R.orbitEquivLogicNat n)
 132
 133/-- Homomorphism from the extracted realization orbit into any Peano object. -/
 134def realizationLift (R : LogicRealization) (B : PeanoObject) :
 135    PeanoObject.Hom (realizationPeano R) B where
 136  toFun := realizationFold R B
 137  map_zero := by
 138    unfold realizationFold
 139    change (logicNatLift B).toFun (R.orbitEquivLogicNat R.orbitZero) = B.zero
 140    rw [R.orbitEquiv_zero]
 141    rfl
 142  map_step := by
 143    intro x
 144    unfold realizationFold
 145    change (logicNatLift B).toFun (R.orbitEquivLogicNat (R.orbitStep x)) =
 146      B.step ((logicNatLift B).toFun (R.orbitEquivLogicNat x))