tickEquivNat_zero

formal source

  66@[simp] theorem tickEquivNat_symm_apply (n : Nat) :
  67    tickEquivNat.symm n = ⟨n⟩ := rfl
  68
  69@[simp] theorem tickEquivNat_zero : tickEquivNat tickZero = 0 := rfl
  70
  71@[simp] theorem tickEquivNat_succ (t : Tick) :
  72    tickEquivNat (tickSucc t) = (tickEquivNat t) + 1 := rfl
  73
  74/-- The canonical equivalence `Tick ≃ LogicNat` via `Nat`. -/
  75def tickEquivLogicNat : Tick ≃ LogicNat :=
  76  tickEquivNat.trans LogicNat.equivNat.symm
  77
  78/-! ## Tick is a natural-number object -/
  79
  80/-- Recursor on `Tick`: iterate `f` from `x` exactly `t.index` times. -/
  81def tickRecursor {X : Type u} (x : X) (f : X → X) (t : Tick) : X :=
  82  Nat.rec x (fun _ acc => f acc) t.index
  83
  84@[simp] theorem tickRecursor_zero {X : Type u} (x : X) (f : X → X) :
  85    tickRecursor x f tickZero = x := rfl
  86
  87@[simp] theorem tickRecursor_succ {X : Type u} (x : X) (f : X → X) (t : Tick) :
  88    tickRecursor x f (tickSucc t) = f (tickRecursor x f t) := rfl
  89
  90/-- **Tick is a Lawvere natural-number object.** Together with `tickZero`
  91and `tickSucc`, the `Tick` type satisfies the universal property of the
  92natural-number object: primitive recursion exists and is unique. -/
  93def tick_isNNO :
  94    IsNaturalNumberObject (N := Tick) tickZero tickSucc where
  95  recursor := fun {X} x f => tickRecursor x f
  96  recursor_zero := fun {X} x f => tickRecursor_zero x f
  97  recursor_step := fun {X} x f t => tickRecursor_succ x f t
  98  recursor_unique := by
  99    intro X x f h hz hs t