Descending into a code

A recursion on codes has to get from a code to its parts, and membership will not take it there. Kuratowski's pair puts a part four membership steps below the tagged code that holds it, and the sets in between are not codes, so an induction on membership cannot carry a hypothesis about codes across them.

Rank can. It increases strictly along membership, so four steps compose into one by transitivity of ordinals, and the recursion then runs on the rank rather than on the code. This chapter is those four steps, once for each side of a pair.

The chapter is small and it is the whole reason the seal on rank exists: a goal mentioning the rank of a pair inside a pair inside a pair took 163 seconds before that seal and 1.4 after.

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

open import Base.Prelude
open import Base.Truth

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

open import FOL.ZFStructure using ( module hPropStructure )
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 ( ∣_∣₁ )
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; SingletonPackage )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ᵥ

The steps

Membership in a singleton and in an unordered pair, stated as the introductions the chain below wants, and the chain itself at four variable sets. Stating it at variables and applying it once is what keeps a proof from unfolding four nested pairs at each of three transitivity steps.

self∈singl : (a : S) → ⟨ a ∈ₛ ⁅ a ⁆s ⟩
self∈singl a = SetPackage.classification (SingletonPackage a) a .snd refl

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

chain4 : (x y z w v : S) → ⟨ x ∈ˢ y ⟩ → ⟨ y ∈ˢ z ⟩ → ⟨ z ∈ˢ w ⟩ → ⟨ w ∈ˢ v ⟩
       → ⟨ rank x ∈ˢ rank v ⟩
chain4 x y z w v x∈y y∈z z∈w w∈v =
  trans≺ x y v x∈y (trans≺ y z v y∈z (trans≺ z w v z∈w (rank-mono w v w∈v)))

Into a tagged payload

A tagged code is a pair whose second component is the payload, and a payload is either a code or a pair of them. So there are three descents to name: into a payload, and into each side of a payload that is a pair. The tag itself is never descended into, which is why it appears as an arbitrary set rather than as a numeral.

payload≺ : (c z : S) → ⟨ rank z ∈ˢ rank (pr c z) ⟩
payload≺ c z = trans≺ z ⁅ c , z ⁆ (pr c z)
  (pair∈ c z z (inr refl))
  (rank-mono ⁅ c , z ⁆ (pr c z) (pair∈ ⁅ c ⁆s ⁅ c , z ⁆ ⁅ c , z ⁆ (inr refl)))

leftPart : (c a b : S) → ⟨ rank a ∈ˢ rank (pr c (pr a b)) ⟩
leftPart c a b = chain4 a ⁅ a ⁆s (pr a b) ⁅ c , pr a b ⁆ (pr c (pr a b))
  (∈∈ₛ {a = a} {b = ⁅ a ⁆s} .snd (self∈singl a))
  (pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a ⁆s (inl refl))
  (pair∈ c (pr a b) (pr a b) (inr refl))
  (pair∈ ⁅ c ⁆s ⁅ c , pr a b ⁆ ⁅ c , pr a b ⁆ (inr refl))

rightPart : (c a b : S) → ⟨ rank b ∈ˢ rank (pr c (pr a b)) ⟩
rightPart c a b = chain4 b ⁅ a , b ⁆ (pr a b) ⁅ c , pr a b ⁆ (pr c (pr a b))
  (pair∈ a b b (inr refl))
  (pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl))
  (pair∈ c (pr a b) (pr a b) (inr refl))
  (pair∈ ⁅ c ⁆s ⁅ c , pr a b ⁆ ⁅ c , pr a b ⁆ (inr refl))