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.

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

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.

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 ℓ.

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.

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.

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.

  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.

  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.

    π-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.

  π-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.

       → Σ[ 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.

  π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.

    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.

  π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.

    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.

      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.

  π∈-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.

    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.

    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.

  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.

      (λ { (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.

  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 ⟩.

    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.

      (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.

    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.

      (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.

      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.

    π-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.

    π∈-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.

    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.

  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.

    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.

      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.

  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.

    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.

        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 ⟩.

          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.

        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.

          (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.