--- title: "The Mostowski collapse" module: V.Collapse lang: en site: "Bedrock" description: "The Mostowski collapse" stage: "Proving GCH" reading_order: 104 canonical: https://bedrock.institute/en/V.Collapse.html html: V.Collapse.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Collapse.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Presentation] routes: [hulls-and-counting] translations: [https://bedrock.institute/zh/V.Collapse.md, https://bedrock.institute/ja/V.Collapse.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The Mostowski collapse Every set of the ambient cumulative hierarchy comes with a canonical presentation: an index type together with an indexing map that names its elements. This chapter asks the converse question. Suppose we single out a set `X` and look only at the elements of the hierarchy that belong to `X`, with the membership relation inherited from the hierarchy. When is this restricted structure, in effect, just another set? The Mostowski collapse answers: membership recursion defines a collapsing map `π`, the range of `π` on `X` is a transitive set, and if `X` satisfies structure extensionality then `π` is injective on `X`, giving an isomorphism between the carrier and its collapsed range. Three mathematical representations shape the proof. First, membership is proposition-valued: the chapter works in a ZF structure `𝒮ᵥ` whose membership predicates take values in propositions, so a membership statement `⟨ z ∈ˢ x ⟩` names an underlying proposition rather than a bare truth value. Second, a set of the hierarchy is used through its small presentation: an index type together with an indexing function `⟪ x ⟫↪` naming the members of `x`, so that building a new set means presenting it with indices. Third, statements about members are often merely true: the propositional truncation `∥_∥₁` turns a statement of the form `some index witnesses this` into the claim that such a witness merely exists, without choosing one. The levels are worth stating exactly. The carrier type `S` of the hierarchy lives in `Type (ℓ-suc ℓ)`, while every presentation index type such as `⟪ x ⟫` is small, in `Type ℓ`; index types and the carrier therefore do not share a universe level. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module V.Collapse {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure; Transitive ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; ∈-induction; ∈-induction-compute ) ``` The three representations interlock. A presentation `sett I f` produces a set whose membership is truncated: a member is given by an index, but membership statements only record that such an index merely exists. This is why later lemmas about `π`'s members conclude with truncated pairs, and why eliminating such a truncation is legitimate there: the target of the elimination, being the proposition underlying a membership statement `⟨ _ ⟩`, is again a proposition, so no chosen witness escapes into data. The equivalence `∈∈ₛ` connects the two memberships in play, native membership of the embedding and membership in the small relation, and is used in both directions to convert membership certificates between their two forms. ```agda open import V.Presentation {ℓ} using ( member; fiber ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) ``` One more representation completes the toolkit: the ambient hierarchy supplies well-founded membership, and with it the principles `∈-induction` and `∈-induction-compute`, which define functions by recursion on membership and record the resulting computation laws; the hierarchy also comes with its own extensionality principle. These drive the collapse: the map `π` will be defined by membership recursion, filtering the members of each set through the carrier `X`. With the representations in place, the first question is what to demand of the carrier `X` itself. ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; _⊆_ ) open hPropStructure 𝒮ᵥ ``` ## Carrier hypotheses The collapse takes a set `X : S` as carrier. Two hypotheses on `X` appear in this chapter, and they play different roles. Transitivity says that members of members of `X` are again in `X`; it is what makes the collapsed range behave well. Structure extensionality says that two elements of `X` with the same members of `X` are equal; it is what makes the collapsing map injective, and it alone suffices for the isomorphism half of the chapter. The transitivity predicate is phrased exactly as in the absoluteness chapter: `Transitive 𝒮ᵥ (λ x → x ∈ˢ u)` says that if `y` is a member of `x` in the structure and `x` is a member of `u` in the small relation, then `y` is a member of `u`. Since the class here is given by small membership in a fixed set `u`, a transitivity witness for `u` is ordinary closure under members of members, and it lives in `Type (ℓ-suc ℓ)` because it quantifies over structure elements and returns propositions at level `ℓ`. ```agda isTrans : S → Type (ℓ-suc ℓ) isTrans u = Transitive 𝒮ᵥ (λ x → x ∈ˢ u) ``` Extensionality is the hypothesis that drives injectivity. Stated for a fixed carrier set `X`, it compares two elements `x` and `y` that both lie in `X`: if every member of `X` that belongs to `x` also belongs to `y` and conversely, then `x ≡ y`. This is a path conclusion, not a biconditional between membership statements. Each quantified member `z` ranges over `X` only: the hypothesis `z ∈ᵗ X` restricts attention to carrier members, so the comparison ignores elements outside `X`. The two inclusion halves are stated separately, each as an implication between truncated membership types `⟨ z ∈ˢ _ ⟩`, and only then does the definition conclude with the path `x ≡ y`. No transitivity of `X` appears in this statement; the injectivity proof later uses `isExt X` alone. ```agda isExt : S → Type (ℓ-suc ℓ) isExt X = (x y : S) → x ∈ᵗ X → y ∈ᵗ X → ((z : S) → z ∈ᵗ X → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩) → ((z : S) → z ∈ᵗ X → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩) → x ≡ y ``` The collapsing map is built once and for all, for an arbitrary carrier `X`. Packaging it in a module parameterized by `X` keeps the carrier explicit in every lemma that follows. Everything from here through the transitivity of the range works for an arbitrary `X : S`; no hypothesis on the carrier is needed until the extensionality section. This is worth noting because the classical statement of the Mostowski collapse often assumes well-foundedness and extensionality up front, while here well-foundedness comes free from the ambient hierarchy, and extensionality enters only where injectivity is proved. ```agda module Collapse (X : S) where ``` ## The recursive collapse For each set `x`, the map `π` should send `x` to the set of collapse values of those members of `x` that also lie in the carrier `X`. This is a definition by recursion on membership: to know `π x` we only need `π y` for members `y` of `x`. Well-foundedness of membership in the ambient hierarchy licenses exactly this form of definition, and also delivers its computation law. The index type `Fiber x` selects the filtered members: an index `m` into the presentation of `x` such that the named element `⟪ x ⟫↪ m` is a small member of `X`. Because the filter uses the small membership, itself a proposition at level `ℓ`, the fiber type lives in `Type ℓ` and the resulting set is legitimately small. The recursive step then presents a new set: indices are the fibers, and each index names `rec` applied to the corresponding member `⟪ x ⟫↪ m` of `x`, together with the membership proof `member x m` that the recursion principle requires to justify the recursive call. Note the direction of information flow: `fiber` is not used here; the carrier-membership witness is carried inside the fiber as data. ```agda Fiber : S → Type ℓ Fiber x = Σ[ m ∈ ⟪ x ⟫ ] ⟨ ⟪ x ⟫↪ m ∈ₛ X ⟩ step : (x : S) → (∀ y → y ∈ᵗ x → S) → S step x rec = sett (Fiber x) (λ p → rec (⟪ x ⟫↪ (p .fst)) (member x (p .fst))) ``` Instantiating the ∈-recursion principle at `step` yields the collapse map `π`. The recursion theorem also provides the equation that unfolds `π x` into the set presented by `step x`, and this equation is what every later argument actually uses. The definition `π = ∈-induction step` is a single appeal to the recursion principle from the hierarchy chapter: since membership is well-founded, a function defined by the recursive step exists on all of `S`. The `opaque` block marks `π` as sealed, meaning the type checker will not unfold it automatically at use sites; this keeps proof terms that mention `π` small. ```agda opaque π : S → S π = ∈-induction step opaque unfolding π ``` Sealing alone would hide the definition, so the second block explicitly allows unfolding of `π` and records the computation law: `π x` is equal, by a path, to the set presented by `step x` with the recursive calls `π y` in place. The law is itself supplied by the companion theorem `∈-induction-compute` from the same recursion principle, so no new proof is needed. Later chapters transport membership proofs across this path rather than unfolding the definition. ```agda π-compute : (x : S) → π x ≡ step x (λ y _ → π y) π-compute = ∈-induction-compute step ``` The first property of `π` describes its members. If `z` belongs to `π x`, then, merely, `z` is the collapse of some element of the carrier. The statement is truncated: we do not choose such an element, we only show that the type of such pairs is inhabited. The proof starts from the membership certificate `z∈` and transports it along the computation law of `π`. After rewriting `π x` into `sett (Fiber x) ⋯`, the membership type of a presented set lets us read off an index: a fiber `p` together with a path showing that `π` of the named member equals `z`. So the computation law converts an abstract membership into concrete recursion data. ```agda π-member : (x z : S) → ⟨ z ∈ˢ π x ⟩ → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁ π-member x z z∈ = PT.map mk (subst (λ w → ⟨ z ∈ˢ w ⟩) (π-compute x) z∈) where mk : Σ[ p ∈ Fiber x ] (π (⟪ x ⟫↪ (p .fst)) ≡ z) ``` The auxiliary function `mk` reshapes this recursion data into the promised form. The witness `⟪ x ⟫↪ (p .fst)` is exactly the member of `x` named by the fiber; the second component `∈∈ₛ ⋯ .snd` converts the fiber's carrier-membership certificate from native to small membership; and the path `q` is reused directly. The result is a truncated pair, built with `PT.map`, so the conclusion remains merely an existence statement even though each ingredient is explicit. ```agda → Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) mk (p , q) = ⟪ x ⟫↪ (p .fst) , ( ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = X} .snd (p .snd) , q ) ``` ## The transitive range The range of the collapse on the carrier deserves to be a set in its own right. Define `πX` by presenting it with the index type of `X`: its members are the collapse values `π (⟪ X ⟫↪ m)` of carrier elements. This section shows that `πX` is transitive, using only that every member of any collapse value is again a collapse of a carrier element, the content of `π-member`. The set `πX` is the image of `π` restricted to `X`, built with `sett` over the index type `⟪ X ⟫` of the carrier's own presentation. Its member lemma is a direct reading of that presentation: a member of `πX` is, merely, `π y` for some `y` in `X`, and the proof simply unpacks the index `m` and repackages the path `π (⟪ X ⟫↪ m) ≡ z` together with the membership certificate `member X m` produced by the presentation's faithfulness. ```agda πX : S πX = sett ⟪ X ⟫ (λ m → π (⟪ X ⟫↪ m)) πX-member : (z : S) → ⟨ z ∈ˢ πX ⟩ → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁ πX-member z z∈ = PT.map mk z∈ ``` The converse introduction says that `πX` contains all the collapse values it should: if `y` is a member of `X`, then `π y` is a member of `πX`. Here the lemma `fiber` from the presentation chapter is essential. A membership proof `y∈X` yields an actual index `m` and a path `⟪ X ⟫↪ m ≡ y`, and applying `cong π` to that path exhibits `π y` as the collapse value at index `m`. Unlike `π-member`, this direction is not truncated in its input; only the output is wrapped in `∥_∥₁` because membership in a presented set is truncated. ```agda where mk : Σ[ m ∈ ⟪ X ⟫ ] (π (⟪ X ⟫↪ m) ≡ z) → Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) mk (m , q) = ⟪ X ⟫↪ m , ( member X m , q ) πX-intro : (y : S) → ⟨ y ∈ˢ X ⟩ → ⟨ π y ∈ˢ πX ⟩ ``` Transitivity of `πX` takes the form demanded by `isTrans`: if `y` is a member of `x` and `x` belongs to the range, then `y` belongs to the range. The proof eliminates the truncated hypothesis `x∈πX` with `PT.rec`, which is legitimate because the goal `⟨ y ∈ˢ πX ⟩` is a proposition. Each witness `z` with `π z ≡ x` and `z ∈ X` reduces the problem to showing `y ∈ π z`. ```agda πX-intro y y∈X = ∣ fiber X y∈X .fst , cong π (fiber X y∈X .snd) ∣₁ πX-trans : isTrans πX πX-trans {x} {y} y∈x x∈πX = PT.rec (snd (y ∈ˢ πX)) go (πX-member x x∈πX) where go : Σ[ z ∈ S ] (⟨ z ∈ˢ X ⟩ × (π z ≡ x)) → ⟨ y ∈ˢ πX ⟩ ``` The inner step first transports `y∈x` along the path `π z ≡ x` to obtain `y ∈ᵗ π z`, then applies `π-member` to see that `y` is, merely, the collapse of some `w` in `X`. Note the asymmetry with the classical picture: the transitivity proof needs no induction on `y`, because membership in the presented set `π z` already exposes the collapse data directly. ```agda go (z , z∈X , pzx) = PT.rec (snd (y ∈ˢ πX)) go₂ (π-member z y y∈πz) where y∈πz : y ∈ᵗ π z y∈πz = subst (λ w → y ∈ᵗ w) (sym pzx) y∈x go₂ : Σ[ w ∈ S ] (⟨ w ∈ˢ X ⟩ × (π w ≡ y)) → ⟨ y ∈ˢ πX ⟩ ``` Finally `go₂` transports the desired membership along the path `π w ≡ y`: since `w` lies in `X`, `πX-intro` gives `⟨ π w ∈ˢ πX ⟩`, and the path identifies `π w` with `y`. With that, `πX-trans` is complete, and the collapse's range is a genuine transitive set. ```agda go₂ (w , w∈X , pwy) = subst (λ v → ⟨ v ∈ˢ πX ⟩) pwy (πX-intro w w∈X) ``` The forward direction records how the collapse respects membership between carrier elements. If `y` is a member of `x` and both lie in the carrier `X`, then `π y` is a member of `π x` in the small relation. This lemma is the workhorse of the isomorphism: both inclusions in the injectivity proof reduce to it. Unlike the truncated `π-member`, here all data is explicit, because the membership `y ∈ᵗ x` itself names a witness. The first ingredient is the fiber of the membership proof. Applying `fiber x` to `yx : y ∈ᵗ x` returns an actual index `m` into the presentation of `x` together with a path `⟪ x ⟫↪ m ≡ y`. This is the same explicit-construction lemma that gave `πX-intro` its witnesses: because the embedding has proposition-valued fibers, the truncated membership can be eliminated into this pair type. ```agda π∈-fwd : (x y : S) → y ∈ᵗ x → y ∈ᵗ X → ⟨ π y ∈ˢ π x ⟩ π∈-fwd x y yx yu = subst (λ w → ⟨ π y ∈ˢ w ⟩) (sym (π-compute x)) wit where fib : Σ[ m ∈ ⟪ x ⟫ ] (⟪ x ⟫↪ m ≡ y) fib = fiber x yx ``` The carrier membership `yu` speaks about `y`, but the fiber pair is built from `⟪ x ⟫↪ m`, so the proof transports `yu` backwards along the path `p` to obtain `⟪ x ⟫↪ m ∈ˢ X`, and then converts that native small-membership certificate into the small relation with the forward half of `∈∈ₛ`. This is the one place where the two memberships meet directly, and `∈∈ₛ` is exactly the bridge. ```agda m : ⟪ x ⟫ m = fib .fst p : ⟪ x ⟫↪ m ≡ y p = fib .snd sm : ⟨ ⟪ x ⟫↪ m ∈ₛ X ⟩ ``` With the pair `(m , sm)` now inhabiting `Fiber x`, the witness `wit` presents `π y` as a member of the set presented by `step x`: the index names the fiber, and the path component is `cong π p`, identifying `π (⟪ x ⟫↪ m)` with `π y`. Transporting along the computation law of `π x` then places this membership under `π x` itself, completing the forward lemma. ```agda sm = ∈∈ₛ {a = ⟪ x ⟫↪ m} {b = X} .fst (subst (λ w → ⟨ w ∈ˢ X ⟩) (sym p) yu) wit : ⟨ π y ∈ˢ sett (Fiber x) (λ q → π (⟪ x ⟫↪ (q .fst))) ⟩ wit = ∣ (m , sm) , cong π p ∣₁ ``` ## Extensionality and the collapse isomorphism With the transitive range in place, the remaining question is whether the carrier survives the collapse without merging. This section assumes the carrier's structure extensionality `isExt X` and proves that `π` is injective on `X`, and consequently that membership between carrier elements agrees in both directions with membership between their collapse values. The key move is a recovery lemma: from `⟨ π z ∈ˢ π x ⟩` and a comparison principle, it reconstructs `z ∈ᵗ x`. Only extensionality enters here; no transitivity of the carrier is needed, since the memberships that a transitivity argument would supply are already carried by the fibers or by the quantification built into `isExt X`. The recovery lemma takes two inputs. The first is the truncated statement `⟨ π z ∈ˢ π x ⟩`; the second is a comparison principle `same` asserting that any `b` in `x ∩ X` with `π b ≡ π z` must equal `z`. The target `z ∈ᵗ x` is a proposition, so eliminating the truncation with `PT.rec` is legitimate. Transporting the hypothesis along the computation law of `π x` turns it into membership in the set presented by `step x`, whose members are indexed by `Fiber x`. ```agda private π∈-recover : (x z : S) → ⟨ π z ∈ˢ π x ⟩ → ((b : S) → b ∈ᵗ x → b ∈ᵗ X → π b ≡ π z → b ≡ z) → z ∈ᵗ x π∈-recover x z h same = PT.rec (snd (z ∈ˢ x)) ``` Given a fiber `p` naming `b = ⟪ x ⟫↪ (p .fst)` as a member of `x`, with the collapse path `π b ≡ π z`, the comparison principle fires. Its hypotheses are discharged directly: `member x (p .fst)` proves `b ∈ᵗ x`, and the second component of `∈∈ₛ` converts the fiber's carrier-membership certificate into `b ∈ᵗ X`. The conclusion `b ≡ z` transports the membership certificate `b ∈ᵗ x` to `z ∈ᵗ x`, which is exactly the goal. ```agda (λ { (p , q) → subst (λ w → ⟨ w ∈ˢ x ⟩) (same (⟪ x ⟫↪ (p .fst)) (member x (p .fst)) (∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = X} .snd (p .snd)) q) (member x (p .fst)) }) (subst (λ w → ⟨ π z ∈ˢ w ⟩) (π-compute x) h) ``` The extensionality-dependent material now lives in a module taking `Xext : isExt X` as a parameter, so that the hypothesis is explicit and is not silently available elsewhere. Inside, the induction predicate `P` is the injectivity statement itself, relative to the carrier: for `x` in `X`, all `y` in `X` with the same collapse value are equal to `x` by a path. This is the property that membership induction will establish for every element of `x` simultaneously. ```agda module InjExt (Xext : isExt X) where P : S → Type (ℓ-suc ℓ) P x = (y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y ``` The two inclusions in the extensionality comparison are proved separately, each by an appeal to the recovery lemma. The first direction moves a member `z` of `x` into `y`: assuming `π x ≡ π y` and the induction hypothesis for members of `x`, it concludes `⟨ z ∈ˢ y ⟩`. To show that `z` belongs to `y`, the recovery lemma is applied with target set `y`: it suffices to know that `π z` is a member of `π y`, and that any `b ∈ y ∩ X` collapsing to `π z` equals `z`. The membership part follows from the forward lemma: since `z` is a member of `x` and both lie in `X`, we have `⟨ π z ∈ˢ π x ⟩`, and the path `e : π x ≡ π y` transports this to `⟨ π z ∈ˢ π y ⟩`. ```agda in⊆ : (x y z : S) → x ∈ᵗ X → y ∈ᵗ X → z ∈ᵗ x → z ∈ᵗ X → π x ≡ π y → ((a : S) → a ∈ᵗ x → P a) → ⟨ z ∈ˢ y ⟩ in⊆ x y z xu yu zx zu e IH = π∈-recover y z ``` The comparison principle is where the induction hypothesis does its work. If `b ∈ y ∩ X` and `π b ≡ π z`, then applying the symmetric path gives `π z ≡ π b`, and the hypothesis `IH z` at the member `z` of `x` produces `z ≡ b`; symmetrizing yields `b ≡ z` as the principle requires. Note that this direction never needs to know that the witness `b` actually exists, only how it would behave. ```agda (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd x z zx zu)) (λ b by bu q → sym (IH z zx b zu bu (sym q))) ``` The second inclusion runs the same argument in the opposite direction, moving a member `z` of `y` into `x`. Combining the two inclusions yields the induction step for injectivity: under the path `π x ≡ π y`, the two sets have exactly the same members of `X`, so structure extensionality concludes `x ≡ y`. The proof is a mirror of `in⊆`: recovery is applied to the target set `x`, and the collapsed membership `⟨ π z ∈ˢ π x ⟩` comes from the forward lemma at the pair `(y, z)` transported along the reversed path `e`. The only asymmetry is the direction of the given path, which accounts for the swapped roles of `x` and `y`. ```agda out⊆ : (x y z : S) → x ∈ᵗ X → y ∈ᵗ X → z ∈ᵗ y → z ∈ᵗ X → π y ≡ π x → ((a : S) → a ∈ᵗ x → P a) → ⟨ z ∈ˢ x ⟩ out⊆ x y z xu yu zy zu e IH = π∈-recover x z ``` The comparison clause here is simpler than in `in⊆`: given `b ∈ x ∩ X` with `π b ≡ π z`, the induction hypothesis `IH b` applies directly at `b` and yields `b ≡ z` without any symmetrizing. The recovery lemma then transports `b ∈ᵗ x` along this path, giving `z ∈ᵗ x`, as required. ```agda (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd y z zy zu)) (λ b bx bu q → IH b bx z bu zu q) step-inj : (x : S) → ((a : S) → a ∈ᵗ x → P a) → P x step-inj x IH y xu yu e = Xext x y xu yu to from where ``` The induction step `step-inj` now assembles the two inclusions into an application of the carrier's extensionality hypothesis `Xext`. Given `x, y ∈ X` and a path `e : π x ≡ π y`, the two clauses `to` and `from` are exactly the comparisons demanded by `isExt X`, each delegating to `in⊆` or `out⊆` with the appropriate orientation of `e`. The conclusion is the path `x ≡ y`, so `P x` holds. ```agda to : (z : S) → z ∈ᵗ X → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩ to z zu zx = in⊆ x y z xu yu zx zu e IH from : (z : S) → z ∈ᵗ X → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩ from z zu zy = out⊆ x y z xu yu zy zu (sym e) IH ``` The injectivity theorem follows by ∈-induction, since each `step-inj` invocation is exactly the induction step for the predicate `P`. No new argument is needed: membership induction on the ambient hierarchy produces, for every `x`, the statement `P x` from the step verified above. Unfolding `P`, this is exactly injectivity of `π` on the carrier: two elements of `X` with equal collapse values are equal. ```agda π-inj : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y π-inj = ∈-induction step-inj ``` With injectivity in hand, the backward direction of the isomorphism follows immediately: a collapsed membership can be traced back to a genuine membership in the carrier. Given `⟨ π y ∈ˢ π x ⟩`, the recovery lemma eliminates a merely existing presentation witness: from a fiber naming some `b ∈ᵗ x` with `π b ≡ π y`, it produces `b ≡ y`, because the comparison clause supplied here applies `π-inj` to conclude the equality outright. Injectivity is what identifies the recovered carrier element with `y`. Transporting the membership certificate of `b` along that path then yields `y ∈ᵗ x`. The elimination is licensed because its target `y ∈ᵗ x` is itself a proposition, being the underlying type of the proposition-valued membership; the witness `b` is never chosen as data, and the conclusion is only the propositional membership statement. ```agda π∈-bwd : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → ⟨ π y ∈ˢ π x ⟩ → y ∈ᵗ x π∈-bwd x y xu yu h = π∈-recover x y h (λ b bx bu q → π-inj b y bu yu q) ``` Assembling both directions gives the isomorphism reading of the collapse: on the carrier, membership and collapsed membership determine each other. The packaged result is a pair of implications, not an equivalence type: from `⟨ y ∈ˢ x ⟩` to `⟨ π y ∈ˢ π x ⟩` via the forward lemma, and back via `π∈-bwd`. This is the precise sense in which the collapse is an isomorphism on the carrier: it preserves and reflects membership among elements of `X`, and by `π-inj` it is injective there. ```agda iso : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → (⟨ y ∈ˢ x ⟩ → ⟨ π y ∈ˢ π x ⟩) × (⟨ π y ∈ˢ π x ⟩ → ⟨ y ∈ˢ x ⟩) iso x y xu yu = (λ yx → π∈-fwd x y yx yu) , π∈-bwd x y xu yu ``` The recursion equation `π x ≡ step x (λ y _ → π y)` is not merely a property of the particular function constructed by `∈-induction`: it characterizes the collapse up to path. Any function `f` satisfying the same recursion equation, with `f` itself in the recursive calls, agrees with `π` everywhere. This uniqueness is what makes the collapse a well-defined object rather than one among possibly many outputs of a construction. The statement quantifies over all `f : S → S` equipped with the computation rule `h : f x ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst)))`. Note the shape: like `π`'s own law, the right-hand side presents a set whose members are the `f`-images of the filtered members of `x`. The conclusion is a path family `π x ≡ f x`, proved by ∈-induction, since knowing the equality on members of `x` determines it at `x`. ```agda unique : (f : S → S) → ((x : S) → f x ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst)))) → (x : S) → π x ≡ f x unique f h = ∈-induction stepU where ``` The induction step chains three paths. Starting from `π-compute x`, the left side becomes the set presented by `step x` with `π` in the recursive calls; the middle path `step-eq` changes the recursive calls from `π` to `f`; and `sym (h x)` unfolds `f x`. The composite exhibits `π x ≡ f x` from the induction hypothesis alone. ```agda stepU : (x : S) → ((y : S) → y ∈ᵗ x → π y ≡ f y) → π x ≡ f x stepU x IH = π-compute x ∙ step-eq ∙ sym (h x) where step-eq : sett (Fiber x) (λ p → π (⟪ x ⟫↪ (p .fst))) ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst))) ``` The middle path itself is congruence applied to the presenting function: `sett` is held fixed while the indexing function changes from `λ p → π (⋯)` to `λ p → f (⋯)`, and `funExt` supplies pointwise equality of these two functions. Each point is an instance of the induction hypothesis, applied at the member named by the fiber `p`, with the membership certificate `member x (p .fst)` justifying the recursive call. This is the standard uniqueness argument for definitions by well-founded recursion, adapted to the presented-set constructor. ```agda step-eq = cong (sett (Fiber x)) (funExt ih') where ih' : (p : Fiber x) → π (⟪ x ⟫↪ (p .fst)) ≡ f (⟪ x ⟫↪ (p .fst)) ih' p = IH (⟪ x ⟫↪ (p .fst)) (member x (p .fst)) ``` When does the collapse change nothing? If `Y` is a transitive subset of the carrier, meaning every member of a member of `Y` again lies in `Y`, then the filter defining the collapse is full on members of `Y`: nothing is discarded, and so `π y ≡ y` for every `y ∈ᵗ Y`. This fixed-point statement is proved by ∈-induction on `y`, comparing `π y` and `y` through the hierarchy's own extensionality principle. The statement combines the two carrier-side data: the inclusion `⟨ Y ⊆ X ⟩` in the small relation and the transitivity `isTrans Y`, which is closure of `Y` under members of members. The induction hypothesis is stated with both memberships visible: it asserts `π m ≡ m` only for members `m` of `y` that also lie in `Y`, matching exactly the situation the proof will encounter. ```agda fixes : (Y : S) → ⟨ Y ⊆ X ⟩ → isTrans Y → (y : S) → y ∈ᵗ Y → π y ≡ y fixes Y YX Ytr = ∈-induction stepF where stepF : (y : S) → ((m : S) → m ∈ᵗ y → m ∈ᵗ Y → π m ≡ m) → y ∈ᵗ Y → π y ≡ y ``` The step compares the two sets through `extensionalV`, the extensionality principle of the hierarchy itself: two sets are equal once they have the same members, formulated here as a family of paths obtained from biconditionals. The direction `to` shows that members of the collapsed set are already members of `y`, and it starts by eliminating the truncated membership `xπ` after transporting it along the computation law, exposing a fiber of `Fiber y` together with the path `π` of the named member equaling `x`. ```agda stepF y IH yY = extensionalV (λ x → ⇔toPath (to x) (from x)) where to : (x : S) → ⟨ x ∈ˢ π y ⟩ → x ∈ᵗ y to x xπ = PT.rec (snd (x ∈ˢ y)) go (subst (λ w → ⟨ x ∈ˢ w ⟩) (π-compute y) xπ) ``` Given such a fiber, the named member `⟪ y ⟫↪ (p .fst)` is a member of `y` that lies in `Y` by transitivity, so the induction hypothesis applies to it and fixes it: `π` of it equals itself. Composing the symmetry of this fixed-point path with the collapse path `q` produces a path from the named member to `x`, and transporting the membership certificate along it lands at `x ∈ᵗ y`. ```agda where go : Σ[ p ∈ Fiber y ] (π (⟪ y ⟫↪ (p .fst)) ≡ x) → x ∈ᵗ y go (p , q) = subst (λ w → ⟨ w ∈ˢ y ⟩) (sym ih' ∙ q) (member y (p .fst)) where ih' : π (⟪ y ⟫↪ (p .fst)) ≡ ⟪ y ⟫↪ (p .fst) ``` The direction `from` shows that every member of `y` survives the collapse. Here transitivity of `Y` is used first, to see that `x` itself lies in `Y`; the induction hypothesis then gives the path `π x ≡ x`, and transporting the forward lemma's conclusion `⟨ π x ∈ˢ π y ⟩` along this path relocates the membership at `x` itself, giving `⟨ x ∈ˢ π y ⟩`. ```agda ih' = IH (⟪ y ⟫↪ (p .fst)) (member y (p .fst)) (Ytr {x = y} {y = ⟪ y ⟫↪ (p .fst)} (member y (p .fst)) yY) from : (x : S) → x ∈ᵗ y → ⟨ x ∈ˢ π y ⟩ from x xy = subst (λ w → ⟨ w ∈ˢ π y ⟩) (IH x xy x∈Y) (π∈-fwd y x xy x∈X) ``` The two auxiliary facts mirror each other. Membership in `Y` comes from transitivity applied to `x ∈ᵗ y` and `y ∈ᵗ Y`. From that, membership in the carrier `X` follows in two small steps: the backward half of `∈∈ₛ` converts `x ∈ᵗ Y` into the small membership statement, and the hypothesis `YX` carries that statement across the inclusion into `X`, where the forward half of `∈∈ₛ` returns an ordinary membership proof. ```agda where x∈Y : x ∈ᵗ Y x∈Y = Ytr {x = y} {y = x} xy yY x∈X : x ∈ᵗ X x∈X = ∈∈ₛ {a = x} {b = X} .snd ``` With both directions established, the biconditional for each `x` is converted into a path by `⇔toPath`, and `extensionalV` assembles the resulting family of paths into `π y ≡ y`. Since `y` was an arbitrary member of `Y`, the collapse fixes `Y` pointwise, closing the induction. ```agda (YX x (∈∈ₛ {a = x} {b = Y} .fst x∈Y)) ``` The fixed-point statement applies in particular when `Y` is the carrier `X` itself: a transitive carrier is fixed pointwise by the collapse, so on such a carrier the collapsing map is the identity.