nno_universal_uniqueness

formal source

  79  ⟨recursor base step, recursor_zero base step, recursor_succ base step⟩
  80
  81/-- The NNO universal property on `LogicNat` in `Type`: uniqueness. -/
  82theorem nno_universal_uniqueness {α : Type*} (base : α) (step : α → α)
  83    (f g : LogicNat → α)
  84    (hf_zero : f LogicNat.zero = base)
  85    (hf_succ : ∀ n, f (LogicNat.succ n) = step (f n))
  86    (hg_zero : g LogicNat.zero = base)
  87    (hg_succ : ∀ n, g (LogicNat.succ n) = step (g n)) :
  88    f = g := by
  89  funext n
  90  induction n with
  91  | identity =>
  92      rw [show LogicNat.identity = LogicNat.zero from rfl, hf_zero, hg_zero]
  93  | step k ih =>
  94      rw [show LogicNat.step k = LogicNat.succ k from rfl, hf_succ k, hg_succ k, ih]
  95
  96/-! ## Master cert -/
  97
  98structure CategoricalMathlibCert where
  99  recursor_zero_eq : ∀ {α : Type*} (base : α) (step : α → α),
 100      recursor base step LogicNat.zero = base
 101  recursor_succ_eq : ∀ {α : Type*} (base : α) (step : α → α) (n : LogicNat),
 102      recursor base step (LogicNat.succ n) = step (recursor base step n)
 103  universal_existence : ∀ {α : Type*} (base : α) (step : α → α),
 104      ∃ (f : LogicNat → α),
 105        f LogicNat.zero = base ∧ ∀ n, f (LogicNat.succ n) = step (f n)
 106  universal_uniqueness : ∀ {α : Type*} (base : α) (step : α → α)
 107      (f g : LogicNat → α),
 108      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
 109      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
 110      f = g
 111
 112theorem categoricalMathlibCert_holds : CategoricalMathlibCert :=