CategoricalMathlibCert

formal source

  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 :=
 113{ recursor_zero_eq := @recursor_zero
 114  recursor_succ_eq := @recursor_succ
 115  universal_existence := @nno_universal_existence
 116  universal_uniqueness := @nno_universal_uniqueness }
 117
 118end
 119
 120end IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib