toPeano

formal source

  59variable {N : Type u} {z : N} {s : N → N}
  60
  61/-- The Peano object carried by a natural-number object. -/
  62def toPeano (_h : IsNaturalNumberObject z s) : PeanoObject where
  63  carrier := N
  64  zero := z
  65  step := s
  66
  67/-- Initiality of an NNO in the category of pointed endomap algebras. -/
  68def isInitial (h : IsNaturalNumberObject z s) :
  69    PeanoObject.IsInitial (toPeano h) where
  70  lift := fun B =>
  71    { toFun := h.recursor B.zero B.step
  72      map_zero := h.recursor_zero B.zero B.step
  73      map_step := fun n => h.recursor_step B.zero B.step n }
  74  uniq := by
  75    intro B f g
  76    funext n
  77    have hf := h.recursor_unique B.zero B.step f.toFun f.map_zero f.map_step n
  78    have hg := h.recursor_unique B.zero B.step g.toFun g.map_zero g.map_step n
  79    rw [hf, hg]
  80
  81end IsNaturalNumberObject
  82
  83/-! ## `LogicNat` is a natural-number object -/
  84
  85/-- `LogicNat` with `identity` and `step` is a Lawvere natural-number object. -/
  86def logicNat_isNNO :
  87    IsNaturalNumberObject (N := LogicNat) LogicNat.identity LogicNat.step where
  88  recursor := fun {X} x f => ArithmeticOf.logicNatFold ⟨X, x, f⟩
  89  recursor_zero := fun _ _ => rfl
  90  recursor_step := fun _ _ _ => rfl
  91  recursor_unique := by
  92    intro X x f h hz hs n