IsInitial

formal source

  55end Hom
  56
  57/-- Initiality of a Peano algebra. This is data, so it lives in `Type`. -/
  58structure IsInitial (A : PeanoObject) where
  59  lift : ∀ B : PeanoObject, Hom A B
  60  uniq : ∀ (B : PeanoObject) (f g : Hom A B), f.toFun = g.toFun
  61
  62end PeanoObject
  63
  64/-- The arithmetic object forced by a Law-of-Logic realization. -/
  65structure ArithmeticOf (R : LogicRealization) where
  66  peano : PeanoObject
  67  initial : PeanoObject.IsInitial peano
  68
  69namespace ArithmeticOf
  70
  71/-- Peano surface of a forced arithmetic object. -/
  72structure PeanoSurface {R : LogicRealization} (A : ArithmeticOf R) : Prop where
  73  zero_ne_step : ∀ x : A.peano.carrier, A.peano.zero ≠ A.peano.step x
  74  step_injective : Function.Injective A.peano.step
  75  induction :
  76    ∀ P : A.peano.carrier → Prop,
  77      P A.peano.zero →
  78      (∀ n, P n → P (A.peano.step n)) →
  79      ∀ n, P n
  80
  81/-! ## LogicNat as the canonical initial Peano object -/
  82
  83/-- The Peano object carried by `LogicNat`. -/
  84def logicNatPeano : PeanoObject where
  85  carrier := LogicNat
  86  zero := LogicNat.zero
  87  step := LogicNat.succ
  88