Set-level recursion on the natural numbers

ZFNat.rec and ZFNat.rec_unique state the universal property of the naturals at the type level: the motive is a Lean family and the recursor is a Lean definition. This file states the same property inside the model: Nat is a ZFSet, arrows are elements of funs, the successor is the set-level function succFun, and composition is ZFSet.composition.

The main result is funs_nat_recursion: for x ∈ X and a step function s ∈ X.funs X there is a unique h ∈ Nat.funs X with h ∅ = x and h ∘ᶻ succFun = s ∘ᶻ h. In categorical terms, (Nat, ∅, succFun) is a natural numbers object in the category of ZFSets and funs.

The successor as a set-level function

noncomputable def ZFSet.succFun : ZFSet.{u_1}

The successor function Nat → Nat, as an element of Nat.funs Nat.

Equations

• ZFSet.succFun = ZFSet.Nat.lambda ZFSet.Nat fun (a : ZFSet.{?u.1}) => insert a a

theorem ZFSet.succFun_is_func : Nat.IsFunc Nat succFun

theorem ZFSet.succFun_is_pfunc : succFun.IsPFunc Nat Nat

theorem ZFSet.succFun_mem_funs : succFun ∈ Nat.funs Nat

theorem ZFSet.fapply_succFun {n : ZFSet.{u_1}} (hn : n ∈ Nat) : @ᶻsuccFun succFun_is_pfunc ⟨n, ⋯⟩ = ⟨insert n n, ⋯⟩

The iterate of a step function

noncomputable def ZFSet.recVal {X : ZFSet.{u_1}} (x s : ZFSet.{u_1}) (hx : x ∈ X) (hs : X.IsFunc X s) : ZFNat → ↥X

The n-th iterate of s applied to x, at the type level. This is ZFNat.rec with the constant motive {y // y ∈ X}; recFun is its transport into the model.

Equations

• ZFSet.recVal x s hx hs n = ZFSet.ZFNat.rec n ⟨x, hx⟩ fun (x : ZFSet.ZFNat) (ih : ↥X) => @ᶻs ⋯ ⟨↑ih, ⋯⟩

theorem ZFSet.recVal_zero {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) : recVal x s hx hs 0 = ⟨x, hx⟩

theorem ZFSet.recVal_succ {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) (n : ZFNat) : recVal x s hx hs n.succ = @ᶻs ⋯ ⟨↑(recVal x s hx hs n), ⋯⟩

The recursor as a set

noncomputable def ZFSet.recFun {X : ZFSet.{u_1}} (x s : ZFSet.{u_1}) (hx : x ∈ X) (hs : X.IsFunc X s) : ZFSet.{u_1}

The set-level recursor: the element of Nat.funs X sending n to sⁿ x.

Equations

• ZFSet.recFun x s hx hs = ZFSet.Nat.lambda X fun (a : ZFSet.{?u.1}) => if hn : a ∈ ZFSet.Nat then ↑(ZFSet.recVal x s hx hs ⟨a, hn⟩) else ∅

theorem ZFSet.recFun_is_func {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) : Nat.IsFunc X (recFun x s hx hs)

theorem ZFSet.recFun_is_pfunc {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) : (recFun x s hx hs).IsPFunc Nat X

recFun as a partial function, so that fapply can be applied to it without re-running the zpfun search on the (large) body of recFun.

theorem ZFSet.recFun_mem_funs {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) : recFun x s hx hs ∈ Nat.funs X

theorem ZFSet.fapply_recFun {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) {n : ZFSet.{u_1}} (hn : n ∈ Nat) : @ᶻ(recFun x s hx hs) ⋯ ⟨n, ⋯⟩ = recVal x s hx hs ⟨n, hn⟩

recFun applied inside the model agrees with the type-level iterate recVal.

The universal property

theorem ZFSet.recFun_zero {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) : ∅.pair x ∈ recFun x s hx hs

recFun sends ∅ — the set-level zero — to x.

theorem ZFSet.recFun_comp_succFun {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) : (recFun x s hx hs).composition succFun Nat Nat X = s.composition (recFun x s hx hs) Nat X X

recFun satisfies the recursion equation h ∘ᶻ succFun = s ∘ᶻ h.

theorem ZFSet.recFun_unique {X x s h : ZFSet.{u_1}} (hx : x ∈ X) (hs : X.IsFunc X s) (hh : Nat.IsFunc X h) (h0 : ∅.pair x ∈ h) (hstep : h.composition succFun Nat Nat X = s.composition h Nat X X) : h = recFun x s hx hs

Uniqueness: any h : Nat → X with h ∅ = x and h ∘ᶻ succFun = s ∘ᶻ h is recFun x s.

The proof is ZFNat.rec_unique — the typed uniqueness lemma — applied to the family fun k ↦ h k, so the set-level statement is discharged by the type-level one.

theorem ZFSet.funs_nat_recursion {X x s : ZFSet.{u_1}} (hx : x ∈ X) (hs : s ∈ X.funs X) : ∃! h : ZFSet.{u_1}, h ∈ Nat.funs X ∧ ∅.pair x ∈ h ∧ h.composition succFun Nat Nat X = s.composition h Nat X X

Set-level recursion theorem for the naturals. For x ∈ X and a step function s ∈ X.funs X there is a unique h ∈ Nat.funs X with h ∅ = x and h ∘ᶻ succFun = s ∘ᶻ h; the witness is recFun x s.

Equivalently: (Nat, ∅, succFun) is a natural numbers object for ZFSets and funs.