tickEquivLogicNat

formal source

  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
 100    -- Reduce to induction on t.index.
 101    suffices hgen : ∀ n : Nat, h ⟨n⟩ = tickRecursor x f ⟨n⟩ by
 102      have := hgen t.index
 103      cases t
 104      exact this
 105    intro n