Rank descent through coded pairs

A later well-founded recursion will proceed over codes and, at each step, process an immediate component of the code it is given. For the recursion to be well-founded it needs a measure that strictly decreases from the code to that component. Membership will not supply one. The Kuratowski pair is defined as pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆: a component such as b is reached only through the intermediate unordered pair ⁅ a , b ⁆, and that intermediate set is not itself a code. An induction on membership therefore cannot carry a hypothesis about codes across them.

Rank can. Rank increases strictly along membership, and its values are ordinals, whose membership is transitive; so a finite membership chain collapses into a single comparison of ordinals, and the recursion can instead be justified by induction on rank. This chapter assembles exactly those comparisons: one step for each side of an ordered pair, and their composition into the four-step descent from each side of a paired payload to the outer tagged code.

The mathematical setting is the cumulative hierarchy: its carrier S, its proposition-valued membership ∈ˢ, and the structure 𝒮ᵥ that packages the set-theoretic operations. One preliminary is worth stating before any descent is proved. A well-founded recursion needs a strict measure, and the measure used later is the von Neumann rank, defined and studied in the chapter on rank; there rank-mono records that rank increases strictly along membership, and rank-ord that every rank is an ordinal.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

module L.Coding.Descent {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

The concrete problem can be seen from the shape of the code. A component of pr a b is not a member of pr a b directly: it is wrapped inside the unordered pair ⁅ a , b ⁆, which in turn is one of the two members of the outer unordered pair. Membership gives a chain of steps rather than one edge, and the links of the chain are sets that carry no code structure at all. What replaces the chain is a strict inequality between ordinals, obtained by translating each membership edge through the rank and then composing.

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Rank {ℓ} using ( rank; rank-mono; rank-ord )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )

The comparison uses three ingredients from the hierarchy: the unordered pair ⁅ u , v ⁆, the pairing axiom pairing-ax, which classifies membership in an unordered pair propositionally, and ∈∈ₛ, which converts membership in the underlying set sense into the structural membership ∈ˢ and back. The sum type _⊎_ will carry the explicit choice between the two components: inl for the left, inr for the right. Keeping the choice explicit rather than merely exists matters here, because the descent proof must pick out which component of the pair is being descended into.

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s )

The crucial distinction is where transitivity is available. Arbitrary set membership is not treated as transitive. After each membership edge has been sent through rank-mono, however, the intermediate objects are ordinals, and rank-ord supplies the transitivity needed to compose their strict inequalities.

open hPropStructure 𝒮ᵥ

The steps

The descent argument rests on two reusable facts. The first is the membership edge into an unordered pair: if w is, explicitly, u or v, then w belongs to ⁅ u , v ⁆. The second is the rank step: one membership edge x ∈ˢ y together with a rank descent from y to z yields a rank descent from x to z. Together they turn chains of membership into single comparisons of ordinals, at arbitrary sets rather than at any particular pair expression.

The pairing axiom classifies membership in ⁅ u , v ⁆ as a truncated disjunction: it is merely the case that a member equals u or equals v. The helper pair∈ produces the reverse direction with the truncation removed: it takes an explicit sum w ≡ u ⊎ w ≡ v and returns a proof of ⟨ w ∈ˢ ⁅ u , v ⁆ ⟩, by inserting ∣ h ∣₁ into the truncated side of pairing-ax and then converting through ∈∈ₛ. This is exactly the direction a descent proof needs: given which component we are descending into, membership follows without any further case analysis. The composition step trans≺ then does the rank translation. Since rank z is an ordinal by rank-ord z, membership below rank z is transitive, so rank x ∈ˢ rank y and rank y ∈ˢ rank z compose into rank x ∈ˢ rank z; the first hypothesis is rank-mono x y applied to x ∈ˢ y. Note that transitivity is used on the ordinal rank, never assumed for membership of arbitrary sets.

pair∈ : (u v w : S) → (w ≡ u) ⊎ (w ≡ v) → ⟨ w ∈ˢ ⁅ u , v ⁆ ⟩
pair∈ u v w h = ∈∈ₛ {a = w} {b = ⁅ u , v ⁆} .snd (pairing-ax u v w .snd ∣ h ∣₁)

trans≺ : (x y z : S) → ⟨ x ∈ˢ y ⟩ → ⟨ rank y ∈ˢ rank z ⟩ → ⟨ rank x ∈ˢ rank z ⟩
trans≺ x y z x∈y ry∈rz = rank-ord z .fst (rank-mono x y x∈y) ry∈rz

Into a tagged payload

With the two steps in hand, the descents for coded pairs follow by reading the shape of the Kuratowski pair. A component x of pr a b reaches the code through two membership edges: x belongs to ⁅ a , b ⁆, and ⁅ a , b ⁆ belongs to pr a b. So pair-component≺ proves the two-step descent for either component, with no condition on the tag. Specializing to the second component gives payload≺, the descent from a payload to its tagged code. A paired payload pr a b under a tag c then needs one more composition, and here the two sides genuinely differ: leftPart descends into the first component inside the payload and then composes with the payload descent, while rightPart simply applies the payload descent twice. Throughout, the tag c is an arbitrary set; nothing requires it to be a numeral or to be descended into.

The two edges are supplied explicitly. For the first, pair∈ a b x h uses the given choice h : x ≡ a ⊎ x ≡ b. For the second, the choice is inr refl: the unordered pair ⁅ a , b ⁆ is definitionally the right member of the outer pair, so pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl) proves its membership in pr a b, and rank-mono turns that into the rank inequality rank ⁅ a , b ⁆ ∈ˢ rank (pr a b). Then trans≺ composes. Note how the middle set ⁅ a , b ⁆ appears only inside this proof: the statement of pair-component≺ mentions nothing but the code and the chosen component. The specialization payload≺ reads z as the right component of pr c z, again by inr refl, giving the descent from a payload to its tagged code for arbitrary tag c.

pair-component≺ : (a b x : S) → (x ≡ a) ⊎ (x ≡ b) → ⟨ rank x ∈ˢ rank (pr a b) ⟩
pair-component≺ a b x h = trans≺ x ⁅ a , b ⁆ (pr a b) (pair∈ a b x h)
  (rank-mono ⁅ a , b ⁆ (pr a b) (pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl)))

payload≺ : (c z : S) → ⟨ rank z ∈ˢ rank (pr c z) ⟩
payload≺ c z = pair-component≺ c z z (inr refl)

Both lemmas under the tag compose at the ordinal rank (pr c (pr a b)), using the transitivity field of rank-ord. The asymmetry between them reflects the nesting. For leftPart, the target a is the first component inside the payload, so the first edge is pair-component≺ a b a (inl refl), giving rank a ∈ˢ rank (pr a b), and the second edge is the payload descent payload≺ c (pr a b). For rightPart, the target b is the second component of the payload itself, so both edges are payload descents: payload≺ a b from b to pr a b, then payload≺ c (pr a b) from the payload to the outer tagged code. In both cases the conclusion has the same shape, rank a or rank b belonging to rank (pr c (pr a b)), which is precisely the measure decrease a later recursion on tagged codes will demand of each immediate component.

leftPart : (c a b : S) → ⟨ rank a ∈ˢ rank (pr c (pr a b)) ⟩
leftPart c a b = rank-ord (pr c (pr a b)) .fst
  (pair-component≺ a b a (inl refl)) (payload≺ c (pr a b))

rightPart : (c a b : S) → ⟨ rank b ∈ˢ rank (pr c (pr a b)) ⟩
rightPart c a b = rank-ord (pr c (pr a b)) .fst (payload≺ a b) (payload≺ c (pr a b))