---
title: "Rank descent through coded pairs"
module: L.Coding.Descent
lang: en
site: "Bedrock"
description: "Rank descent through coded pairs"
stage: "Internal coding: expressions and domains"
reading_order: 45
canonical: https://bedrock.institute/en/L.Coding.Descent.html
html: L.Coding.Descent.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Descent.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Coding, L.Rank]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.Descent.md, https://bedrock.institute/ja/L.Coding.Descent.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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`.

```agda
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.

```agda
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))
```