BedrockRead this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapThis chapter builds the environment tower inside L. For each natural number n, the tower records the coded ordered pair (# n, envSet W n), where envSet W n is the set of all length-n environments taking values in W. The construction first produces the actual set and then gives a bounded first-order description through which later chapters can read its coded entries.
{-# OPTIONS --cubical --safe --guardedness #-}
The construction is carried out in cubical type theory and uses excluded middle at the stated universe level. This classical hypothesis enters through the constructions of fixed-length environment sets, common bounds, separation, and the internal natural numbers.
open import Base.Prelude open import Base.Classical using ( LEM )
Fix a universe level ℓ and an instance lem : LEM (ℓ-suc ℓ). Every construction below is relative to this one hypothesis; no stronger classical principle is added.
module L.Coding.EnvironmentTower {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
Two descriptions of the tower will coexist. The first is an external construction of a set in L; the second is a formula in the object language of set theory. Membership, equality, conjunction, disjunction, and bounded quantification form that formula, while the Lévy-hierarchy checker will certify that it is Δ₀.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ⊥̇; ∃̇_; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ ) import FOL.Absoluteness
The proof later reads a tower entry downward to a predecessor. Membership induction in the cumulative hierarchy justifies this descent, and extensionality identifies environment sets once their members agree. Injectivity of the coded ordered pair then recovers the numeral and environment-set components separately.
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV ) open import V.Coding {ℓ} using ( pr; pr-inj ) open import V.Model {ℓ} using ( self∈sucV ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Environment {ℓ} using ( env; cons )
The bridge between the two descriptions consists of formulas recognizing coded pairs, von Neumann successors, environment sets, and cons extensions. Containers keep the component quantifiers bounded, and adequacy lemmas identify satisfaction of these formulas with the corresponding constructions in the cumulative hierarchy.
open import L.Coding.Model {ℓ} using ( prAtL; prʟ; prʟ-fst; container ) open import L.Coding.Expressions {ℓ} using ( envSetAt; sucAtL; consAtL; consAtL-adequate; numL ) open import L.Coding.Quantification {ℓ} using ( i0; i1; i2; i3; sh; pr-out; pr-in; down; suc-out; suc-in
Reading and constructing a coded pair repeatedly requires access to both components. The two-component quantifiers provide this access inside bounded formulas, and their introduction and elimination lemmas preserve the propositional nature of satisfaction. The family envSet W n supplies the semantic sets to which those components will be compared.
; i4; i5 ; sndEx; bothEx; bothAll ; sndEx-out; bothEx-out; bothAll-in ; fillSnd; fillBoth; useBoth ) open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in; envSet-out; envS; Ix )
An environment-set formula determines a set only extensionally. Its agreement theorem compares that description with the constructed envSet W n. A common bound and full separation will then collect all arities into one constructible set, while constructible numerals provide its first components.
open import L.Coding.EnvironmentAgreement {ℓ} lem using ( module Ambient; module AmbientHolds ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Axioms.Basic {ℓ} using ( extensionalL ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
The internal set ωʟ connects an object-language arity with an external natural number. Reading one of its members yields, under propositional truncation, a natural number and an identification with the corresponding constructible numeral. It therefore establishes that some arity exists without choosing one globally for every member.
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
Finite vectors represent the environments in which formulas are interpreted, while dependent pairs and coproducts express the witnesses and case distinctions returned by their semantics. Natural-number addition accounts for the extra slots introduced by bounded pair readers.
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.Unit using ( tt ) open import Cubical.Data.Vec using ( _∷_; []; lookup ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Data.Sum using ( _⊎_; inl; inr )
Many semantic witnesses in this chapter live under propositional truncation. Such a witness may be used when the target is itself a proposition, as happens for membership, satisfaction, and equality between hierarchy sets, but it cannot be projected into a globally chosen arity or environment. Propositional extensionality and the empty type support the corresponding equality and impossibility arguments.
open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
A set in the cumulative hierarchy comes with a small presentation of its members. Passing between membership and the corresponding fibre lets the proof turn an arbitrary member of W into a presentation index. The same hierarchy supplies the von Neumann numerals # n and their successor operation sucV.
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet {ℓ} using ( #_; sucV )
Write S for the type of constructible sets. An element of S consists of an underlying hierarchy set together with evidence that it lies in L; the proofs below compare underlying sets through the first projection while preserving this evidence when constructing witnesses.
open hPropStructure 𝒮ʟ using ( S )
Formula satisfaction is interpreted over vectors of constructible sets. Transitivity of L connects this internal interpretation with the ambient cumulative hierarchy, so the same underlying membership facts can support both the object-language formulas and the external construction.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
Constructing the tower set
With that interpretation fixed, the first task is to collect all arity-indexed environment sets into one set.
The tower module fixes the carrier W whose members are the values environments may take. Its n-th entry is the coded ordered pair of the constructible numeral n and the set of all environments of length n: the first component records the length, the second collects all environments of exactly that length.
module Tower (W : S) where entry : ℕ → S entry n = prʟ (numeralL n) (envSet W n)
The entries are first gathered into a common container by the small-domain principle. The container is only a shared upper bound; the precise collection is carved out by separation next.
private dom : Σ[ d ∈ S ] ((k : Lift {ℓ-zero} {ℓ} ℕ) → ⟨ fst (entry (lower k)) ∈ fst d ⟩) dom = smallDom (Lift {ℓ-zero} {ℓ} ℕ) (λ k → entry (lower k))
The separating formula decomposes a candidate into an arity and an environment set and imposes four conditions: the base-set witness equals W; the candidate is the coded ordered pair of the arity and that set; the arity belongs to the internal ω; and the set satisfies the first-order, extensional description envSetAt at that arity over W. Its three leading existential quantifiers are unbounded, so this formula is used with full separation rather than the later Δ₀ argument.
towerFo : Formula S 1 towerFo = ∃̇ (∃̇ (∃̇ ( (var i2 ≐ con W) ∧̇ ( prAtL i3 i1 i0 ∧̇ ( (var i1 ∈̇ con ωʟ) ∧̇ envSetAt i0 i1 i2 )))))
The tower is carved by separation out of the container and kept opaque, so later arguments use it only through its membership specification.
opaque tower : S tower = hasSeparationL (dom .fst) towerFo .fst .fst
The membership specification is exported: membership in the tower is membership in the container conjoined with satisfaction of the separating formula.
tower-mem : (x : S) → (fst x ∈ fst tower) ≡ ((fst x ∈ fst (dom .fst)) ⊓ ((x ∷ []) ⊨ towerFo)) tower-mem = hasSeparationL (dom .fst) towerFo .fst .snd
The key ingredient is that each environment set satisfies its own external description at its own entry: the environment set, its numeral, the carrier, and the entry are placed in a four-slot environment, and the description is satisfied there by construction.
private holdsAt : (n : ℕ) → ⟨ (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ []) ⊨ envSetAt i0 i1 i2 ⟩ holdsAt n = AmbientHolds.holds W (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ []) i0 i1 i2 n refl (numeralL-fst n) refl
Every standard entry therefore belongs to the tower: the container membership is supplied by the bounding record, and the separating formula is satisfied by the truncated witness built from the carrier, the numeral, and the environment set.
tower-in : (n : ℕ) → ⟨ fst (entry n) ∈ fst tower ⟩ tower-in n = subst ⟨_⟩ (sym (tower-mem (entry n))) ( dom .snd (lift n) , ∣ W , ∣ numeralL n , ∣ envSet W n , ( refl
The witness tree nests the carrier, the constructible numeral, and the environment set, and each level transports its own component: the ordered pair is recognized through the pairing projection law, the numeral membership through the internal ω reading, and the description by the ingredient above.
, ( pr-in i3 i1 i0 (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ []) (prʟ-fst (numeralL n) (envSet W n)) , ( subst ⟨_⟩ (sym (ω-specL (numeralL n))) ∣ lift n , refl ∣₁ , holdsAt n ))) ∣₁ ∣₁ ∣₁ )
The standard entry is then restated in ambient normal form: the coded pair of the constructible numeral and the environment set has the same underlying ordered pair as the plain pair of the numerals and the underlying stage, by the two projection laws.
tower-in′ : (n : ℕ) → ⟨ pr (# n) (fst (envSet W n)) ∈ fst tower ⟩ tower-in′ n = subst (λ u → ⟨ u ∈ fst tower ⟩) (prʟ-fst (numeralL n) (envSet W n) ∙ cong (λ u → pr u (fst (envSet W n))) (numeralL-fst n)) (tower-in n)
Conversely, membership in the constructed tower can be read out: every member is merely the coded pair of a numeral and the environment set of that length. The natural number and the equality are returned under propositional truncation, so this result records existence without defining a choice of arity for every member. The proof first unfolds the membership specification and retains its separating-formula component.
tower-out : (x : S) → ⟨ fst x ∈ fst tower ⟩ → ∥ Σ[ n ∈ ℕ ] (fst x ≡ pr (# n) (fst (envSet W n))) ∥₁ tower-out x hx = PT.rec squash₁ byB (subst ⟨_⟩ (tower-mem x) hx .snd) where Goal : Type (ℓ-suc ℓ)
The target type makes that boundary explicit: it is the propositional truncation of a natural number n together with an equality from the member’s underlying set to the standard pair pr (# n) (fst (envSet W n)).
Goal = ∥ Σ[ n ∈ ℕ ] (fst x ≡ pr (# n) (fst (envSet W n))) ∥₁
The separating formula binds three witnesses. The first elimination names the base-set witness b; the remaining formula will identify it with W while also exposing the arity and environment-set witnesses.
byB : Σ[ b ∈ S ] ⟨ (b ∷ x ∷ []) ⊨ ∃̇ (∃̇ ( (var i2 ≐ con W) ∧̇ ( prAtL i3 i1 i0 ∧̇ ( (var i1 ∈̇ con ωʟ) ∧̇ envSetAt i0 i1 i2 )))) ⟩ → Goal byB (b , hb) = PT.rec squash₁ byN hb
The second elimination names the arity as a constructible set.
where byN : Σ[ n ∈ S ] ⟨ (n ∷ b ∷ x ∷ []) ⊨ ∃̇ ( (var i2 ≐ con W) ∧̇ ( prAtL i3 i1 i0 ∧̇ ( (var i1 ∈̇ con ωʟ) ∧̇ envSetAt i0 i1 i2 ))) ⟩ → Goal
The third elimination names the environment set and exposes the four conjuncts: the base set is W, the ordered pair is recognized, the arity is in the internal ω, and the external description of the environment set holds.
byN (n , hn) = PT.rec squash₁ byE hn where byE : Σ[ F ∈ S ] ⟨ (F ∷ n ∷ b ∷ x ∷ []) ⊨ ( (var i2 ≐ con W) ∧̇ ( prAtL i3 i1 i0 ∧̇ ( (var i1 ∈̇ con ωʟ)
The ordered-pair reader recovers the equality from the member to the coded pair of the arity and the described set. Membership of the arity in the internal ω then yields, under propositional truncation, an ordinary natural number whose constructible numeral has the same underlying set.
∧̇ envSetAt i0 i1 i2 ))) ⟩ → Goal byE (F , (qb , (hp , (hω , hE)))) = PT.rec squash₁ byK (subst ⟨_⟩ (ω-specL n) hω) where xq : fst x ≡ pr (fst n) (fst F) xq = pr-out i3 i1 i0 (F ∷ n ∷ b ∷ x ∷ []) hp
The numeral identification aligns the recorded arity with the constructible numeral of the natural number, and the environment-agreement module is opened at the four-slot environment, prepared to compare the described set with the constructed one.
byK : Σ[ k ∈ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] (fst n ≡ fst (numeralL (lower k))) → Goal
byK (k , qn) = ∣ lower k , xq ∙ cong₂ pr (qn ∙ numeralL-fst (lower k)) Eq ∣₁
where
module Am = Ambient W (F ∷ n ∷ b ∷ x ∷ []) i0 i1 i2 (lower k)
(qn ∙ numeralL-fst (lower k)) qb hE using (into; outof)
The agreement module supplies both directions of membership between the described set and the constructed environment set, and extensionality inside L converts these two directions into an equality of underlying sets.
Eq : fst F ≡ fst (envSet W (lower k)) Eq = cong fst (extensionalL {a = F} {b = envSet W (lower k)} (λ z → ⇔toPath (Am.into z) (Am.outof z)))
A bounded specification of the tower
The emptiness predicate says that a set has no members at all, by a bounded universal over its members.
emptyAll : ∀ {m} → Fin m → Formula S m emptyAll x = ∀̇∈ (var x) ⊥̇
The singleton-of-empty clause has two conjuncts: the set contains an empty member, and every member of it is empty. Both are needed: the first is an existence clause, and without it the predicate would also hold of the empty set itself.
sglEmpty : ∀ {m} → Fin m → Formula S m sglEmpty F = ∃̇∈ (var F) (emptyAll i0) ∧̇ ∀̇∈ (var F) (emptyAll i0)
The cons-image clause gives both inclusions needed for equality. Every member of the proposed successor set must merely be a cons of some carrier element onto some member of the predecessor set. Conversely, for every predecessor environment and every carrier element, a corresponding cons extension must merely occur in the successor set. Together these conditions say that the successor set has exactly the cons extensions and no additional members.
consImage : ∀ {m} → Fin m → Fin m → Fin m → Formula S m consImage F' F w = ∀̇∈ (var F') (∃̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F)) (consAtL i2 i1 i0))) ∧̇ ∀̇∈ (var F) (∀̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F')) (consAtL i0 i1 i2)))
The two bodies describe one adjacent step after the current entry has been decomposed into an arity and an environment set. upBody says that the new arity is the successor of the current arity and that the new environment set is its cons image. downBody reverses these roles: the current arity is the successor of the predecessor arity, and the current environment set is the cons image of the predecessor set.
private upBody downBody : ∀ {m} → Fin m → Formula S (8 + m) upBody w = sucAtL i5 i1 ∧̇ consImage i0 i4 (sh 8 w) downBody w = sucAtL i1 i5 ∧̇ consImage i4 i0 (sh 8 w)
The upward clause exists over the tower: some entry of the tower satisfies the upward body.
towerUp : ∀ {m} → Fin m → Fin m → Formula S (4 + m) towerUp E w = ∃̇∈ (var (sh 4 E)) (bothEx i0 (upBody w))
The downward clause is a disjunction: the entry equals the base entry with an empty environment set, or some tower entry is a predecessor whose cons image is the current one. This is what supports the membership-induction reading below.
towerDown : ∀ {m} → Fin m → Fin m → Fin m → Formula S (4 + m) towerDown E w N0 = ((var i1 ≐ var (sh 4 N0)) ∧̇ sglEmpty i0) ∨̇ ∃̇∈ (var (sh 4 E)) (bothEx i0 (downBody w))
The full formula conjoins three bounded conditions on coded ordered-pair entries: a base pair occurs in E; every member of E that is read through the pair interface has an upward successor; and every such pair is either a base pair or has a predecessor. Thus towerAt controls the coded ordered-pair entries used by the later readers. It does not by itself exclude arbitrary non-pair members of E, nor does this chapter derive equality of an arbitrary satisfying E with the constructed Tower.tower W.
towerAt : ∀ {m} → Fin m → Fin m → Fin m → Formula S m towerAt E w N0 = ∃̇∈ (var E) (sndEx i0 (sh 1 N0) (sglEmpty i0)) ∧̇ ( ∀̇∈ (var E) (bothAll i0 (towerUp E w)) ∧̇ ∀̇∈ (var E) (bothAll i0 (towerDown E w N0)) )
The Δ₀ certificate is produced by the checker. It certifies only that every quantifier is bounded; the semantic correctness of the formula is established by the reading lemmas below, not by this certificate.
Δ₀-towerAt : ∀ {m} (E w N0 : Fin m) → Δ₀ (towerAt E w N0) Δ₀-towerAt E w N0 = checkΔ₀ (towerAt E w N0) tt
The zero and successor environment sets
The facts module fixes the carrier W and collects the concrete recursion facts about zero-length and successor-length environments.
module EnvFacts (W : S) where private ι : ⟪ fst W ⟫ → V ℓ ι = ⟪ fst W ⟫↪
Every presented index names a member of W: the small membership bridge runs from the presentation into the underlying set.
ι∈ : (q : ⟪ fst W ⟫) → ⟨ ι q ∈ fst W ⟩ ι∈ q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)
There is exactly one index of length zero, and it is recognized because a function out of an empty type is defined by its impossible cases.
g0 : Ix W 0 g0 ()
A set with no members equals the zero-length environment graph, by extensionality: neither side has a member, since the zero-length index has no cases.
noMembers→env0 : (z : V ℓ) → ((y : V ℓ) → ⟨ y ∈ z ⟩ → Empty.⊥) → z ≡ fst (envS W g0) noMembers→env0 z k = extensionalV (λ y → ⇔toPath (λ hy → Empty.rec (k y hy)) (PT.rec (snd (y ∈ z)) (λ { (lift () , _) })))
Conversely, every environment graph of length zero has no members: the index has no cases, so the pair that would encode a member cannot be formed.
envAny0-noMembers : (g : Ix W 0) (y : V ℓ) → ⟨ y ∈ fst (envS W g) ⟩ → Empty.⊥ envAny0-noMembers g y = PT.rec Empty.isProp⊥ (λ { (lift () , _) })
Reading the zero-length environment set out: every member is a set with no members. The proof eliminates the truncated presentation and applies the previous fact.
envSet0-out : (z : V ℓ) → ⟨ z ∈ fst (envSet W 0) ⟩ → (y : V ℓ) → ⟨ y ∈ z ⟩ → Empty.⊥ envSet0-out z hz y hy = PT.rec Empty.isProp⊥ (λ { (g , e) → envAny0-noMembers g y (subst (λ u → ⟨ y ∈ u ⟩) e hy) }) (envSet-out W 0 (down (envSet W 0) z hz) hz)
Filling the zero-length environment set uses the empty set: it is transported into the presentation, and the empty graph is recognized from its no-members proof.
envSet0-in : (z : V ℓ) → ((y : V ℓ) → ⟨ y ∈ z ⟩ → Empty.⊥) → ⟨ z ∈ fst (envSet W 0) ⟩ envSet0-in z k = subst (λ u → ⟨ u ∈ fst (envSet W 0) ⟩) (sym (noMembers→env0 z k)) (envSet-in W g0)
The environment coding agrees with cons at the function level: prepending a carrier element and shifting the indices codes exactly the cons of the coded functions, entry by entry.
cons-env : (q : ⟪ fst W ⟫) {k : ℕ} (g : Ix W k) → env (cons (ι q) (λ i → ι (g i))) ≡ fst (envS W (cons q g)) cons-env q g = cong env (funExt (λ { zero → refl ; (suc i) → refl }))
Every carrier element extends every environment of length k to an environment of length suc k: the new member of W is presented by an index, and the extended function is inserted into the successor environment set.
envCons∈ : {k : ℕ} (x : V ℓ) → ⟨ x ∈ fst W ⟩ → (g : Ix W k) → ⟨ env (cons x (λ i → ι (g i))) ∈ fst (envSet W (suc k)) ⟩ envCons∈ {k} x x∈ g = subst (λ u → ⟨ u ∈ fst (envSet W (suc k)) ⟩) (sym (cong (λ v → env (cons v (λ i → ι (g i)))) (sym (fib .snd)) ∙ cons-env (fib .fst) g))
The presenting index is recovered from the membership through the fiber of the presentation, so the coding uses the actual presenting index of x.
(envSet-in W (cons (fib .fst) g)) where fib : Σ[ q ∈ ⟪ fst W ⟫ ] (ι q ≡ x) fib = ∈-asFiber {a = x} {b = fst W} x∈
The insertion is restated for a constructible element with an identification of its underlying set: membership in the successor environment set follows by transporting along that identification.
envSuc-in : {k : ℕ} (x e' : S) → ⟨ fst x ∈ fst W ⟩ → (g : Ix W k) → fst e' ≡ env (cons (fst x) (λ i → ι (g i))) → ⟨ fst e' ∈ fst (envSet W (suc k)) ⟩ envSuc-in {k} x e' x∈ g qe' = subst (λ u → ⟨ u ∈ fst (envSet W (suc k)) ⟩) (sym qe') (envCons∈ (fst x) x∈ g)
A successor environment splits at the function level into a head and a tail. If g' indexes a successor environment, then its underlying set equals the coded graph of the function whose zero-th entry is the head value ι (g' zero) and whose i+1-st entry is ι (g' (suc i)). The proof is the functoriality of the environment constructor under the function extensionality that says the two index functions agree at every slot.
env-split : {k : ℕ} (g' : Ix W (suc k)) → fst (envS W g') ≡ env (cons (ι (g' zero)) (λ i → ι (g' (suc i)))) env-split g' = cong env (funExt (λ { zero → refl ; (suc i) → refl }))
The outward reading of a successor environment recovers its head and tail only under propositional truncation. For each member e' of envSet W (suc k), there merely exist a presentation index q naming a member ι q of W, a tail index g : Ix W k, and an equality identifying the underlying set of e' with the coded graph of their cons function.
envSuc-out : {k : ℕ} (e' : S) → ⟨ fst e' ∈ fst (envSet W (suc k)) ⟩ → ∥ Σ[ q ∈ ⟪ fst W ⟫ ] Σ[ g ∈ Ix W k ] (fst e' ≡ env (cons (ι q) (λ i → ι (g i)))) ∥₁ envSuc-out {k} e' h = PT.map (λ { (g' , e) → g' zero , (λ i → g' (suc i)) , (e ∙ env-split g') })
The membership proof is consumed by the outward reading of the environment set, which supplies the truncated index; the equation of the graph then composes with the splitting lemma to produce the cons equation.
(envSet-out W (suc k) e' h)
Reading the successor construction
The cons-image reader is parameterized by the candidate successor set F', the candidate base set F, the alphabet slot w, and the environment, together with the equation aligning the alphabet slot with the working set.
module ConsImageRead {m : ℕ} (F' F w : Fin m) (γ : S ^ m) (W : S) (qw : fst (lookup w γ) ≡ fst W) where open EnvFacts W private ι : ⟪ fst W ⟫ → V ℓ
The embedding of the carrier into the hierarchy is named once, so that every carrier element can be presented as a hierarchy element when needed by the coding.
ι = ⟪ fst W ⟫↪
For each q in the carrier of W, the presentation map places ι q in the underlying set of W. The proof reads membership from the fibre supplied by the canonical presentation of that set.
ι∈' : (q : ⟪ fst W ⟫) → ⟨ ι q ∈ fst W ⟩ ι∈' q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)
The outward reading of the cons-image clause says: if the base set equals the stage environment set at k, then a set satisfying the cons-image clause equals the successor stage environment set. The proof is by extensionality, comparing members in two directions.
The forward direction reads a member z of the candidate successor set through the cons-image clause.
consImage-out : (k : ℕ) → fst (lookup F γ) ≡ fst (envSet W k) → ⟨ γ ⊨ consImage F' F w ⟩ → fst (lookup F' γ) ≡ fst (envSet W (suc k)) consImage-out k qF (h1 , h2) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z)) where fwd : (z : V ℓ) → ⟨ z ∈ fst (lookup F' γ) ⟩ → ⟨ z ∈ fst (envSet W (suc k)) ⟩
The clause supplies a carrier element x and a coded environment entry e and the cons equation; the environment-set outward reading at the base set supplies a truncated index g. Each truncated witness is eliminated into the next proposition.
fwd z hz = PT.rec (snd (z ∈ fst (envSet W (suc k)))) (λ { (x , (x∈ , hx)) → PT.rec (snd (z ∈ fst (envSet W (suc k)))) (λ { (e , (e∈ , hc)) → PT.rec (snd (z ∈ fst (envSet W (suc k)))) (λ { (g , qe) → envSuc-in x zS (subst (λ u → ⟨ fst x ∈ u ⟩) qw x∈) g
In the forward inclusion, the first half of the cons-image clause supplies a head x, a tail environment e, and satisfaction of the coded cons relation. Reading e in the actual base environment set yields a tail index under propositional truncation. Adequacy of consAtL then identifies z with the semantic cons graph, and envSuc-in places that graph in envSet W (suc k). Every truncation is eliminated into this membership proposition.
(subst ⟨_⟩ (consAtL-adequate i2 i1 i0 (e ∷ x ∷ zS ∷ γ) (λ i → ι (g i)) qe) hc) }) (envSet-out W k e (subst (λ u → ⟨ fst e ∈ u ⟩) qF e∈)) }) hx }) (h1 zS hz) where
The membership proof for z in the candidate successor set supplies a constructible representative zS : S with underlying set z. This representative is the value passed to the bounded cons-image reader.
zS : S zS = down (lookup F' γ) z hz
For the reverse inclusion, take a member z of the actual successor environment set. Its successor decomposition merely supplies a head q, a tail index g, and an equation identifying z with their cons environment. The second half of the cons-image clause then merely supplies a corresponding member e' of the candidate successor set.
bwd : (z : V ℓ) → ⟨ z ∈ fst (envSet W (suc k)) ⟩ → ⟨ z ∈ fst (lookup F' γ) ⟩ bwd z hz = PT.rec (snd (z ∈ fst (lookup F' γ))) (λ { (q , g , qz) → PT.rec (snd (z ∈ fst (lookup F' γ))) (λ { (e' , (e'∈ , hc)) → subst (λ u → ⟨ u ∈ fst (lookup F' γ) ⟩)
The adequacy of consAtL identifies the object-language cons relation supplied by the clause with the same coded cons graph used in the semantic decomposition. Composing this equation with the decomposition equation identifies e' with z, so membership of e' transports to membership of z.
(subst ⟨_⟩ (consAtL-adequate i0 i1 i2 (e' ∷ xS q ∷ envS W g ∷ γ) (λ i → ι (g i)) refl) hc ∙ sym qz) e'∈ }) (h2 (envS W g) (subst (λ u → ⟨ fst (envS W g) ∈ u ⟩) (sym qF) (envSet-in W g)) (xS q) (subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q))) })
The two propositional truncations are eliminated only into the membership proposition being proved. The element zS presents z inside the constructible carrier, while xS will similarly present the recovered head.
(envSuc-out zS hz) where zS : S zS = down (envSet W (suc k)) z hz xS : ⟪ fst W ⟫ → S
For a recovered head q, its image ι q lies in W; transitivity of constructibility therefore equips it with the certificate needed to form the carrier element xS q.
xS q = ι q , isL-trans {x = fst W} {y = ι q} (ι∈' q) (snd W)
The inward direction of the cons-image clause is proved from the two identifications with the actual stage environment sets. Both directions of the cons-image clause are now available.
consImage-in : (k : ℕ) → fst (lookup F γ) ≡ fst (envSet W k) → fst (lookup F' γ) ≡ fst (envSet W (suc k)) → ⟨ γ ⊨ consImage F' F w ⟩ consImage-in k qF qF' = h1 , h2 where
The first direction of the inward reading says that every member of the candidate successor set satisfies the bounded existential: there exists a head element and an environment from the base set whose cons extension is the member.
The truncated decomposition of the member is consumed to name the head and the tail.
h1 : (e' : S) → ⟨ fst e' ∈ fst (lookup F' γ) ⟩ → ⟨ (e' ∷ γ) ⊨ ∃̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F)) (consAtL i2 i1 i0)) ⟩ h1 e' he' = PT.map (λ { (q , g , qe') → let xS : S
The head is carried into the carrier, the tail is presented as an element of the base set by the base-set membership identification, and the cons adequacy transports the cons equation into the object language.
xS = ι q , isL-trans {x = fst W} {y = ι q} (ι∈' q) (snd W) in xS , ( subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q) , ∣ envS W g , ( subst (λ u → ⟨ fst (envS W g) ∈ u ⟩) (sym qF) (envSet-in W g) , subst ⟨_⟩ (sym (consAtL-adequate i2 i1 i0 (envS W g ∷ xS ∷ e' ∷ γ) (λ i → ι (g i)) refl)) qe' ) ∣₁ ) }) (envSuc-out e' (subst (λ u → ⟨ fst e' ∈ u ⟩) qF' he'))
The second clause starts with a member e of the base set and a member x of the alphabet set. It must merely exhibit a member of the candidate successor set whose coded graph is obtained by adjoining x to the environment represented by e.
The outward reading of the base environment set merely supplies the tail index g; the semantic cons introduction then places the resulting graph in the actual successor environment set.
h2 : (e : S) → ⟨ fst e ∈ fst (lookup F γ) ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup w γ) ⟩
→ ⟨ (x ∷ e ∷ γ) ⊨ ∃̇∈ (var (sh 2 F')) (consAtL i0 i1 i2) ⟩
h2 e he x hx = PT.map
(λ { (g , qe) →
let m : ⟨ env (cons (fst x) (λ i → ι (g i))) ∈ fst (envSet W (suc k)) ⟩
The constructed environment is presented as an element of the successor stage environment set by descending along the membership supplied by the cons introduction. The cons adequacy transports the satisfaction of the cons clause into the object language.
m = envCons∈ (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qw hx) g e' : S e' = down (envSet W (suc k)) (env (cons (fst x) (λ i → ι (g i)))) m in e' , ( subst (λ u → ⟨ fst e' ∈ u ⟩) (sym qF') m , subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i2 (e' ∷ x ∷ e ∷ γ) (λ i → ι (g i)) qe)) refl ) })
The base-set outward reading supplies the truncated index g whose environment is the entry e.
(envSet-out W k e (subst (λ u → ⟨ fst e ∈ u ⟩) qF he))
Numerals are presented as constructible elements: the finite ordinal together with its constructibility certificate.
nn : ℕ → S nn k = # k , numL k
Reading the tower specification
The single-empty-set module is parameterized by the candidate set slot and the environment.
module SglEmpty (W : S) {m : ℕ} (F : Fin m) (γ : S ^ m) where open EnvFacts W
The outward reading says that a set satisfying the single-empty-set clause has the same underlying set as the zero-stage environment set. The proof is by extensionality, comparing members in two directions.
The first named object is the underlying set of the candidate, and the none helper extracts a refutation from the bounded clause.
sglEmpty-out : ⟨ γ ⊨ sglEmpty F ⟩ → fst (lookup F γ) ≡ fst (envSet W 0) sglEmpty-out (hex , hall) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z)) where Fv = fst (lookup F γ) none : (z : S) → ⟨ (z ∷ γ) ⊨ emptyAll i0 ⟩ → (y : V ℓ) → ⟨ y ∈ fst z ⟩ → Empty.⊥
The none helper feeds a carrier presentation of a member into the bounded clause, which returns the empty type, confirming that the presented set has no members.
none z k y hy = Empty.rec* (k (down z y hy) hy)
Forward: a member of the candidate set is presented, the bounded clause refutes every member of it, so it has no members; the zero-stage introduction then admits it as a member of the zero-stage environment set.
fwd : (z : V ℓ) → ⟨ z ∈ Fv ⟩ → ⟨ z ∈ fst (envSet W 0) ⟩ fwd z hz = envSet0-in z (none (down (lookup F γ) z hz) (hall (down (lookup F γ) z hz) hz))
Backward: a member of the zero-stage environment set is presented, and its truncated index is consumed. Both the indexed environment and the member itself are shown to have no members, so they are equal by extensionality of the hierarchy.
bwd : (z : V ℓ) → ⟨ z ∈ fst (envSet W 0) ⟩ → ⟨ z ∈ Fv ⟩ bwd z hz = PT.rec (snd (z ∈ Fv)) (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Fv ⟩) (noMembers→env0 (fst e) (none e he) ∙ sym (noMembers→env0 z (envSet0-out z hz)))
The transported membership closes the backward direction, and the existence clause completes the proof by confirming the candidate is nonempty.
e∈ }) hex
For the inward reading, choose the empty environment e0. The existential half is satisfied because e0 belongs to the zero-stage environment set and has no members. The universal half follows because every member of that environment set has no members. Transport along the assumed equality replaces the actual zero-stage set by the candidate set in both halves.
sglEmpty-in : fst (lookup F γ) ≡ fst (envSet W 0) → ⟨ γ ⊨ sglEmpty F ⟩ sglEmpty-in q = ∣ e0 , ( subst (λ u → ⟨ fst e0 ∈ u ⟩) (sym q) (envSet-in W (λ ())) , (λ y hy → lift (envAny0-noMembers (λ ()) (fst y) hy)) ) ∣₁ , (λ z hz y hy → lift (envSet0-out (fst z) (subst (λ u → ⟨ fst z ∈ u ⟩) q hz) (fst y) hy))
The empty environment is the coded graph of the function from the empty type, which has no entries.
where e0 : S e0 = envS W (λ ())
The tower reader fixes a candidate tower slot E, a parameter-set slot w, a zero-numeral slot N0, and an interpreting environment. Its hypotheses identify w with the working set W, identify N0 with # 0, and assert satisfaction of towerAt E w N0. The two readings below are relative to exactly these identifications.
module TowerRead {m : ℕ} (E w N0 : Fin m) (γ : S ^ m) (W : S) (qw : fst (lookup w γ) ≡ fst W) (qN0 : fst (lookup N0 γ) ≡ # 0) (h : ⟨ γ ⊨ towerAt E w N0 ⟩) where private Ev = fst (lookup E γ)
The three conjuncts of the tower formula are named: the base clause, the upward-closure clause, and the downward-decomposition clause.
hbase = h .fst hup = h .snd .fst hdown = h .snd .snd
An entry is a truncated record of a natural number arity and an environment set whose underlying set is presented by that arity. It is the reading goal for the tower's outward direction.
Entry : V ℓ → V ℓ → Type (ℓ-suc ℓ) Entry n F = ∥ Σ[ k ∈ ℕ ] ((n ≡ # k) × (F ≡ fst (envSet W k))) ∥₁
The outward reading of tower entries is proved by membership induction on the first component of the encoded pair. The motive says: for every hierarchy element nv, whenever the first component of an entry equals nv and the entry belongs to the candidate tower, the entry decomposes as a natural-number arity with its environment set. This is a well-founded induction on the membership relation of the hierarchy, not an ordinary induction on natural numbers.
The step function splits on the downward-decomposition clause of the tower formula.
entry-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ Ev ⟩ → Entry (fst n) (fst F) entry-out n F = ∈-induction {P = P} step (fst n) n F refl where P : V ℓ → Type (ℓ-suc ℓ) P nv = (n F : S) → fst n ≡ nv → ⟨ pr (fst n) (fst F) ∈ Ev ⟩ → Entry (fst n) (fst F)
The step of the membership induction splits on the downward-decomposition clause of the tower formula, which says that the pair either is the base entry or has a predecessor entry.
step : (nv : V ℓ) → ((y : V ℓ) → ⟨ y ∈ nv ⟩ → P y) → P nv
step nv IH n F qn p∈ = PT.rec squash₁ cases
(useBoth i0 (pS ∷ γ) n F refl (towerDown E w N0) (hdown pS p∈))
where
pS : S
The membership proof for the candidate pair supplies a constructible representative pS : S. Its container exposes the numeral and environment-set components through bounded quantification, and the four-slot environment places those components beside the pair and the surrounding chapter environment.
pS = down (lookup E γ) (pr (fst n) (fst F)) p∈ c = container pS n F refl δ : S ^ (4 + m) δ = F ∷ n ∷ c .fst ∷ pS ∷ γ
The case split consumes the downward-decomposition satisfaction. The base case reads the zero-numeral equation together with the single-empty-set outward reading, producing the arity zero and the zero-stage environment set. The successor case passes to the recursive step.
cases : ((fst n ≡ fst (lookup N0 γ)) × ⟨ δ ⊨ sglEmpty i0 ⟩) ⊎ ⟨ δ ⊨ ∃̇∈ (var (sh 4 E)) (bothEx i0 (downBody w)) ⟩ → Entry (fst n) (fst F) cases (inl (qn0 , hF)) = ∣ 0 , (qn0 ∙ qN0 , SglEmpty.sglEmpty-out W i0 δ hF) ∣₁ cases (inr hs) = PT.rec squash₁
The successor case unpacks the bounded existentials: a predecessor entry p' and a successor equation, followed by a predecessor numeral n', a predecessor environment set F', a cons container, and the cons equation. The four-slot extension prepares the induction.
The ordinality comparison says the candidate numeral is the von Neumann successor of the predecessor numeral.
(λ { (p' , (p'∈ , hb)) → PT.rec squash₁ (λ { (n' , F' , s' , (qp' , (hsuc , hci))) → let δ' = F' ∷ n' ∷ s' ∷ p' ∷ δ qsuc : fst n ≡ sucV (fst n') qsuc = suc-out i1 i5 δ' hsuc
The predecessor numeral lies in the candidate numeral because every set lies in its von Neumann successor; transport along the successor equation makes this the strict descent required by membership induction. Applying the induction hypothesis recovers an arity k and the stage envSet W k.
n'∈ : ⟨ fst n' ∈ nv ⟩ n'∈ = subst (λ u → ⟨ fst n' ∈ u ⟩) (sym qsuc ∙ qn) (self∈sucV (fst n')) in PT.map (λ { (k , (qk , qF')) → suc k , ( qsuc ∙ cong sucV qk
The recovered arity is mapped to its successor, and the cons-image outward reading transports the base environment set to the successor environment set. The induction hypothesis is applied at the predecessor, whose membership is transported along the tower equation.
, ConsImageRead.consImage-out i4 i0 (sh 8 w) δ' W qw k qF' hci ) }) (IH (fst n') n'∈ n' F' refl (subst (λ u → ⟨ u ∈ Ev ⟩) qp' p'∈)) }) (bothEx-out i0 (downBody w) (p' ∷ δ) hb) }) hs
The inward reading is proved by ordinary induction on the external natural number k. At zero, the base clause merely supplies a tower member together with its second component. Reading sglEmpty identifies that component with envSet W 0, while the alignment N0 = # 0 identifies the first component; transport along the resulting pair equation yields the standard zero entry.
entry-in : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩ entry-in zero = PT.rec (snd (pr (# 0) (fst (envSet W 0)) ∈ Ev)) (λ { (p , (p∈ , hs)) → PT.rec (snd (pr (# 0) (fst (envSet W 0)) ∈ Ev)) (λ { (F , s , (qp , hF)) → subst (λ u → ⟨ u ∈ Ev ⟩)
After the zero case closes, the successor step applies the upward-closure clause to the already constructed standard entry at k. That clause merely supplies a new tower member together with a numeral satisfying the successor formula and an environment set satisfying the cons-image formula.
(qp ∙ cong₂ pr qN0 (SglEmpty.sglEmpty-out W i0 (F ∷ s ∷ p ∷ γ) hF)) p∈ }) (sndEx-out i0 (sh 1 N0) (sglEmpty i0) (p ∷ γ) hs) }) hbase entry-in (suc k) = PT.rec (snd (pr (# (suc k)) (fst (envSet W (suc k))) ∈ Ev))
The successor formula determines the new first component from the old numeral, and the outward reading of the cons-image formula determines the new second component from envSet W k. Applying the coded-pair equation to these two identifications yields the standard successor entry (# (suc k), envSet W (suc k)).
(λ { (p' , (p'∈ , hb)) → PT.rec (snd (pr (# (suc k)) (fst (envSet W (suc k))) ∈ Ev)) (λ { (n' , F' , s' , (qp' , (hsuc , hci))) → let δ' = F' ∷ n' ∷ s' ∷ p' ∷ δ in subst (λ u → ⟨ u ∈ Ev ⟩) (qp' ∙ cong₂ pr (suc-out i5 i1 δ' hsuc)
The induction hypothesis first supplies membership of the standard entry at k. Applying upward closure to that entry merely produces a successor entry together with its two component formulas. Their outward readings identify the components with # (suc k) and envSet W (suc k), so transport along the resulting coded-pair equality proves membership of the standard successor entry.
(ConsImageRead.consImage-out i0 i4 (sh 8 w) δ' W qw k refl hci)) p'∈ }) (bothEx-out i0 (upBody w) (p' ∷ δ) hb) }) (useBoth i0 (pS ∷ γ) (nn k) (envSet W k) refl (towerUp E w) (hup pS (entry-in k))) where
To invoke upward closure, the standard entry at k is first presented as the carrier element pS. Its container exposes the two components to bounded quantification, and the four-slot environment records the current environment set, numeral, container, and tower entry.
pS : S pS = down (lookup E γ) (pr (# k) (fst (envSet W k))) (entry-in k) c = container pS (nn k) (envSet W k) refl δ : S ^ (4 + m) δ = envSet W k ∷ nn k ∷ c .fst ∷ pS ∷ γ
The tower-holding module assumes that the candidate tower has been identified with the real tower by an equation of underlying sets, in addition to the carrier and numeral equations. All conclusions are relative to these identifications.
module TowerHolds {m : ℕ} (E w N0 : Fin m) (γ : S ^ m) (W : S) (qw : fst (lookup w γ) ≡ fst W) (qE : fst (lookup E γ) ≡ fst (Tower.tower W)) (qN0 : fst (lookup N0 γ) ≡ # 0) where private Ev = fst (lookup E γ)
Every standard entry belongs to the candidate tower, by transporting the real tower's inward reading along the identification equation.
entry∈ : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩
entry∈ k = subst (λ u → ⟨ pr (# k) (fst (envSet W k)) ∈ u ⟩) (sym qE) (Tower.tower-in′ W k)
Each standard entry is presented as a carrier element by descending along its membership in the candidate tower.
entryS : (k : ℕ) → S entryS k = down (lookup E γ) (pr (# k) (fst (envSet W k))) (entry∈ k)
Every member of the candidate tower is read as a standard entry, by transporting the membership into the real tower and applying the tower's outward reading.
read : (p : S) → ⟨ fst p ∈ Ev ⟩ → ∥ Σ[ k ∈ ℕ ] (fst p ≡ pr (# k) (fst (envSet W k))) ∥₁ read p p∈ = Tower.tower-out W p (subst (λ u → ⟨ fst p ∈ u ⟩) qE p∈)
The tower-holding conclusion is the triple of clauses: the base clause, the upward-closure clause, and the downward-decomposition clause. The base clause is proved by presenting the zero-th standard entry and its membership.
holds : ⟨ γ ⊨ towerAt E w N0 ⟩ holds = hbase , (hup , hdown) where hbase : ⟨ γ ⊨ ∃̇∈ (var E) (sndEx i0 (sh 1 N0) (sglEmpty i0)) ⟩ hbase = ∣ entryS 0 , ( entry∈ 0
The zero-th entry is filled with its numeral equation, its membership, and the single-empty-set inward reading applied to the presented environment. The numeral equation is transported from the candidate zero-numeral slot.
, fillSnd i0 (entryS 0 ∷ γ) (lookup N0 γ) (envSet W 0) (cong (λ a → pr a (fst (envSet W 0))) (sym qN0)) (sglEmpty i0) (SglEmpty.sglEmpty-in W i0 (envSet W 0 ∷ container (lookup i0 (entryS 0 ∷ γ)) (lookup N0 γ) (envSet W 0)
The base clause is now complete. Its witness is the canonical entry entryS 0, whose membership in E comes from the alignment with the constructed tower. The equation qN0 aligns the first component with the designated zero slot, while SglEmpty.sglEmpty-in identifies the second component with the singleton containing the empty environment. Hence the required base entry exists, still under propositional truncation.
(cong (λ a → pr a (fst (envSet W 0))) (sym qN0)) .fst ∷ entryS 0 ∷ γ) refl) (sh 1 N0) refl ) ∣₁
For upward closure, fix an entry p of E and any coded-pair presentation p = (n,F) supplied to bothAll-in. The reader read p p∈ says, under propositional truncation, that p is the canonical entry (# k, envSet W k) for some k. Injectivity of the ordered-pair code then identifies n with # k and F with envSet W k. Thus the argument uses precisely the coded ordered-pair interface controlled by towerAt.
hup : (p : S) → ⟨ fst p ∈ Ev ⟩ → ⟨ (p ∷ γ) ⊨ bothAll i0 (towerUp E w) ⟩ hup p p∈ = bothAll-in i0 (towerUp E w) (p ∷ γ) (λ n F s s∈ n∈ F∈ e → PT.rec (snd ((F ∷ n ∷ s ∷ p ∷ γ) ⊨ towerUp E w)) (λ { (k , qp) → let q = pr-inj (sym e ∙ qp)
The next canonical entry is obtained from the membership proof for entryS (suc k) in E. The environment δ1 records this entry together with the components F and n of the current entry; container then supplies the bounded container needed to expose the numeral and environment-set components of the new ordered pair. Extending once more to δ2 places the canonical successor numeral and envSet W (suc k) in the slots required by upBody.
δ1 = entryS (suc k) ∷ F ∷ n ∷ s ∷ p ∷ γ c' = container (lookup i0 δ1) (nn (suc k)) (envSet W (suc k)) refl δ2 = envSet W (suc k) ∷ nn (suc k) ∷ c' .fst ∷ δ1 in ∣ entryS (suc k) , ( entry∈ (suc k) , fillBoth i0 δ1 (nn (suc k)) (envSet W (suc k)) refl (upBody w)
The two conjuncts of upBody now express the two successor steps. The introduction lemma for sucAtL uses the first-component equality, transported through sucV, to relate # (suc k) to the new numeral slot. Independently, ConsImageRead.consImage-in uses the second-component equality, the alignment w = W, and the adequacy of consAtL to show that envSet W (suc k) is exactly the cons image of envSet W k. These proofs produce a truncated successor-entry witness; eliminating the truncated result of read into that satisfaction proposition establishes upward closure for every entry.
( suc-in i5 i1 δ2 (cong sucV (sym (q .fst))) , ConsImageRead.consImage-in i0 i4 (sh 8 w) δ2 W qw k (q .snd) refl ) ) ∣₁ }) (read p p∈))
Downward decomposition begins in the same way: fix an entry p, choose any coded-pair presentation p = (n,F), and use read only through propositional truncation. A resulting witness supplies some natural number k for which p = (# k, envSet W k). Pattern matching on this witness separates k = 0 from k = suc j, exactly the two disjuncts of towerDown.
hdown : (p : S) → ⟨ fst p ∈ Ev ⟩ → ⟨ (p ∷ γ) ⊨ bothAll i0 (towerDown E w N0) ⟩ hdown p p∈ = bothAll-in i0 (towerDown E w N0) (p ∷ γ) (λ n F s s∈ n∈ F∈ e → PT.rec (snd ((F ∷ n ∷ s ∷ p ∷ γ) ⊨ towerDown E w N0)) (λ { (zero , qp) → let q = pr-inj (sym e ∙ qp)
If k is zero, injectivity of the ordered-pair code identifies n with # 0 and F with envSet W 0. The first equality, combined with qN0, proves that the recorded numeral is the designated zero, while SglEmpty.sglEmpty-in turns the second equality into the singleton-of-empty condition. This establishes the left disjunct. If k = suc j, the same injectivity instead recovers the predecessor index and its environment set; the next environments prepare a witness for the right disjunct.
in ∣ inl (q .fst ∙ sym qN0 , SglEmpty.sglEmpty-in W i0 (F ∷ n ∷ s ∷ p ∷ γ) (q .snd)) ∣₁ ; (suc j , qp) → let q = pr-inj (sym e ∙ qp) δ1 = entryS j ∷ F ∷ n ∷ s ∷ p ∷ γ c' = container (lookup i0 δ1) (nn j) (envSet W j) refl
For the successor case, entryS j supplies the canonical predecessor entry in E. The introduction lemma for sucAtL uses the first-component equality to show that the current numeral is the successor of the predecessor numeral. Then ConsImageRead.consImage-in, using w = W and the second-component equality, proves that the current environment set is the cons image of the predecessor environment set. Packaging the predecessor and these two facts gives the truncated witness required by the right disjunct.
δ2 = envSet W j ∷ nn j ∷ c' .fst ∷ δ1 in ∣ inr ∣ entryS j , ( entry∈ j , fillBoth i0 δ1 (nn j) (envSet W j) refl (downBody w) ( suc-in i1 i5 δ2 (q .fst) , ConsImageRead.consImage-in i4 i0 (sh 8 w) δ2 W qw j refl (q .snd) ) ) ∣₁ ∣₁ })
Eliminating the truncated result of read into the satisfaction proposition completes downward decomposition for every member of the real tower. Together with the base and upward clauses, this proves towerAt E w N0 whenever E, w, and N0 are aligned with Tower.tower W, W, and # 0. The conclusion establishes the bounded description for the real tower while retaining the coded ordered-pair boundary of the formula.
(read p p∈))
Recap
The environment tower now has both forms needed later: an actual constructible set whose members are exactly the standard pairs (# n, envSet W n), and a Δ₀ formula that reads and produces its coded ordered-pair entries one adjacent arity at a time. The two directions use different inductions: membership induction rules out endless descent when reading an entry, while ordinary induction on natural numbers constructs every standard entry. All recovered arities and decompositions remain under propositional truncation, and the formula makes no claim about possible non-pair members of an arbitrary candidate set.