The Mostowski collapse

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 index type lives in Type ℓ and the resulting set is legitimately small. The recursive step then presents a new set: indices are the index pairs, 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 index pair 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: an index pair 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∈ = 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 index pair; the second component ∈∈ₛ ⋯ .snd converts the index pair's carrier-membership certificate from native to small membership; and the path q is reused directly. The result is a truncated pair, built with 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∈ = 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 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 = rec₁ ((y ∈ˢ πX) .snd) 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) = rec₁ ((y ∈ˢ πX) .snd) 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 an element of the presentation map’s fibre over y, recovered from 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 fibres, 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 index 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: its index is this pair, 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 index pairs 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 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 = rec₁ ((z ∈ˢ x) .snd)

Given an index pair 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 index pair'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

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

  (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd x z zx zu))
  (λ b by bu q → sym (IH z zx b zu bu (sym q)))

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

  (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

  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

π-inj : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y
π-inj = ∈-induction step-inj

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

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 index pair 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 an element 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π = rec₁ ((x ∈ˢ y) .snd) go
      (subst (λ w → ⟨ x ∈ˢ w ⟩) (π-compute y) xπ)

Given such an index pair, 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))