IsNaturalNumberObject

formal source

  46This characterization makes no reference to `Nat`. It is the universal
  47property that any Peano structure must satisfy. The field name `recursor`
  48avoids the reserved `rec` symbol used for auto-generated structure recursors. -/
  49structure IsNaturalNumberObject {N : Type u} (z : N) (s : N → N) where
  50  recursor : ∀ {X : Type u}, X → (X → X) → N → X
  51  recursor_zero : ∀ {X : Type u} (x : X) (f : X → X), recursor x f z = x
  52  recursor_step : ∀ {X : Type u} (x : X) (f : X → X) (n : N),
  53    recursor x f (s n) = f (recursor x f n)
  54  recursor_unique : ∀ {X : Type u} (x : X) (f : X → X) (h : N → X),
  55    h z = x → (∀ n, h (s n) = f (h n)) → ∀ n, h n = recursor x f n
  56
  57namespace IsNaturalNumberObject
  58
  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]