---
title: "Collapsing a transitive well-founded relation"
module: L.Mostowski
lang: en
site: "Bedrock"
description: "Collapsing a transitive well-founded relation"
stage: "Ordinals, injections and cardinals"
reading_order: 95
canonical: https://bedrock.institute/en/L.Mostowski.html
html: L.Mostowski.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Mostowski.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, L.Constructible]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/L.Mostowski.md, https://bedrock.institute/ja/L.Mostowski.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Collapsing a transitive well-founded relation

How much set-theoretic structure does a relation carry on its own? Fix a small type `A` with a well-founded, transitive relation `_≺_` valued in `Type ℓ`. Mostowski's answer: the relation alone determines a function `col : A → SV.S` by recursion, with

`col p = { col r | r ≺ p }`,

so each point is sent to the set of collapse values of its predecessors. A computation rule characterizes membership in each value, and transitivity of the relation makes every collapse value an ordinal in the sense used here, a transitive set all of whose members are transitive.

A finite example shows the mechanism. Take three points `s`, `r`, `p` with `s ≺ r`, `r ≺ p`, and, by transitivity, `s ≺ p`, and with no other relations. Then `col s` has no members forced by the recursion, `col r = { col s }`, and `col p = { col s, col r }`, and this is exactly the von Neumann picture of `0`, `1`, `2`. The recursion never inspects the points themselves, only their cones of predecessors.

Three features of the setting shape everything that follows. First, `A` and each fiber `x ≺ y` live in `Type ℓ`, so for each `p` the predecessor cone is the small type `Σ[ r ∈ A ] (r ≺ p)`; the `sett` constructor of the hierarchy `V` turns precisely such a small family into a set of `SV.S`. Second, membership in a `sett`-set is by construction a propositional truncation: `⟨ b ∈ˢ a ⟩` says that some index of the family merely hits `b`, not that a chosen index is available. The chapter therefore proves membership in one direction from given data (`r ≺ p` yields `col r ∈ˢ col p`) and, in the other direction, only a merely existing predecessor with an equation of collapse values. Third, the targets of the later eliminations are propositions, such as an equality of sets or `isTransV x`, so eliminating the truncation into them is legitimate. No extensionality hypothesis on `_≺_` appears, so two points with identical predecessor cones are not distinguished: the collapse is canonical, but not claimed to be injective. The construction uses only well-founded recursion and transport; no classical principle is assumed anywhere in this module.

The collapse lands in the set-level carrier of the cumulative hierarchy, so its output is made of genuine sets rather than of points of `A`. That carrier, written `SV.S` below, is a type whose equality types are propositions, and its membership `_∈ˢ_` packages each membership statement as an `hProp`: an underlying type `⟨ b ∈ˢ a ⟩` together with a proof that this type is a proposition. Working against this fixed vocabulary, the chapter's theorems can state membership and transitivity with the hierarchy's own relation rather than with a new one.

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

open import Base.Prelude

module L.Mostowski {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

Two ingredients drive the construction. The first is the image operation `sett` of the hierarchy: from a small index type `X` and a family `X → V ℓ` it forms the set of that family's values, with membership holding merely when some index hits the target. The second is the well-foundedness certificate `WellFounded _≺_`, the assertion that every element of `A` is accessible along `≺`; its induction principle builds recursively defined functions, and its companion computation law records what such a function does at each point. Propositional truncation enters through `∥ _ ∥₁` with introduction `∣ _ ∣₁`, because membership in an image is truncated by design. The ordinal target `IsOrd`, transitivity `isTransV`, and its propositionhood proof `isPropIsTransV` come from the development of `L` and appear only at the end, where the final theorem needs them.

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; isTransV; isPropIsTransV )

open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.Induction.WellFounded using ( WellFounded; module WFI )
import Cubical.HITs.PropositionalTruncation as PT
```

The hierarchy structure has equality and membership valued in `hProp` at level `ℓ-suc ℓ`. Independently, `A` and every fiber `x ≺ y` lie in `Type ℓ`, so each predecessor cone is a small index type to which `sett` applies. These size facts are all the construction needs; no excluded-middle hypothesis occurs.

```agda
open PT using ( ∣_∣₁; ∥_∥₁ )

module SV = hPropStructure 𝒮ᵥ
open SV using ( _∈ˢ_ )
```

The construction now has two tasks. First, derive the two membership laws for the collapse: a given predecessor produces a member, while a member reflects to a merely existing predecessor with the same collapse value. Second, use those laws in well-founded induction to prove `IsOrd (col p)` for every `p`. The asymmetry between explicit input and truncated output is essential in both tasks.

Well-foundedness is what licenses the recursion. The induction principle obtained from `wf` says that, to define a family `P` on `A`, it suffices at each `p` to construct `P p` from values of `P` at every predecessor `r ≺ p`. The transitivity witness `≺-trans` is not needed to define `col`; it enters later when proving that the resulting sets are transitive.

```agda
module Mostowski (A : Type ℓ) (_≺_ : A → A → Type ℓ)
                 (wf : WellFounded _≺_)
                 (≺-trans : {x y z : A} → x ≺ y → y ≺ z → x ≺ z) where

  module W = WFI wf using ( induction; induction-compute )

  colStep : (p : A) → (∀ r → r ≺ p → SV.S) → SV.S
```

The recursion step is the image of the predecessor cone. Given `p` and a recursive call `rec` that already knows `col r` for each `r ≺ p`, the step forms `sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z))`: the index type is the total space of pairs `(r , r ≺ p)`, and the family sends such a pair to `rec r`. Abstractly this is exactly the set `{ col r | r ≺ p }`, the collapsing equation the chapter announced. Note how the step type quantifies over arbitrary step functions `rec`, which is what makes the same data serve both the definition and, via the computation law below, reasoning about it.

```agda
  colStep p rec = sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z))

  opaque
    col : A → SV.S
    col = W.induction {P = λ _ → SV.S} colStep

    col-eq : (p : A) → col p ≡ sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → col (fst z))
```

The function `col` is defined by well-founded induction. Its computation rule `col-eq` identifies `col p` with the image of the predecessor cone under `col` itself. Later membership proofs use this equality to pass between the recursively defined value and the explicit image, where membership has the truncated-preimage classification supplied by `sett`.

```agda
    col-eq = W.induction-compute colStep

  col-in : (p r : A) → r ≺ p → ⟨ col r ∈ˢ col p ⟩
  col-in p r rp =
    subst (λ v → ⟨ col r ∈ˢ v ⟩) (sym (col-eq p)) ∣ (r , rp) , refl ∣₁

  col-out : (p : A) (b : SV.S) → ⟨ b ∈ˢ col p ⟩
```

Membership admits a computation law in each direction, and the two are usefully asymmetric. Forward: if `r ≺ p` is given, then `col r` is a member of `col p`. The witness is the pair `(r , rp)` together with the path `refl` recording that `col r` is hit at index `r`; transporting along `col-eq p` (in the form `sym`, since the equation was proved in the other direction) moves this member of the explicit image into the type `⟨ col r ∈ˢ col p ⟩`. Backward: an arbitrary membership `⟨ b ∈ˢ col p ⟩` yields only the truncated statement that some `r ≺ p` merely exists with `col r ≡ b`. The proof transports the membership along `col-eq p` back to membership in the explicit image, which is by construction a truncated preimage, then relabels the index data as a predecessor with an equation. Nothing here selects a specific `r`; the truncation `∥ _ ∥₁` is the honest record of what membership reveals.

```agda
          → ∥ Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ b)) ∥₁
  col-out p b b∈ =
    PT.map (λ z → fst (fst z) , snd (fst z) , snd z)
      (subst (λ v → ⟨ b ∈ˢ v ⟩) (col-eq p) b∈)

  col-ord : (p : A) → IsOrd (col p)
```

The final theorem says every collapse value is an ordinal, where `IsOrd (col p)` unpacks to a pair: `col p` is transitive, and each of its members is transitive. The proof runs by well-founded induction on `p`, so the induction hypothesis `rec` provides `IsOrd (col r)` for every predecessor `r ≺ p`, and the goal is assembled from its two components. This is the one place where the hypothesis `≺-trans` earns its keep; before reading the two clauses, picture a three-point chain `s ≺ r ≺ p`: transitivity of the relation is exactly what lets membership facts about `col r` be replayed inside `col p`.

```agda
  col-ord = W.induction {P = λ p → IsOrd (col p)} ih
    where
    ih : (p : A) → (∀ r → r ≺ p → IsOrd (col r)) → IsOrd (col p)
    ih p rec = tr , mem
      where
```

The first clause, that every member of `col p` is transitive, starts from `col-out p x x∈`: the member `x` is `col r` for some merely existing predecessor `r ≺ p`, with an equation `e : col r ≡ x`. The induction hypothesis supplies `isTransV (col r)`, and `subst isTransV e` transports that proof along the equation to type `isTransV x`. The elimination of the truncation is legitimate because the target `isTransV x` is a proposition, certified by `isPropIsTransV x`; no witness is being extracted, only a proposition is being established from a merely existing case analysis.

```agda
      mem : (x : SV.S) → ⟨ x ∈ˢ col p ⟩ → isTransV x
      mem x x∈ = PT.rec (isPropIsTransV x)
        (λ z → subst isTransV (snd (snd z)) (rec (fst z) (fst (snd z)) .fst))
        (col-out p x x∈)
      tr : isTransV (col p)
```

The second clause proves `col p` itself transitive: given `y ∈ x` and `x ∈ col p`, show `y ∈ col p`. First peel `x ∈ col p` through `col-out`, obtaining merely some `r ≺ p` with `col r ≡ x`. The equation transports the given `y ∈ x` into `⟨ y ∈ˢ col r ⟩`, which is where the running example's middle link `r` finally connects the two ends of the chain.

```agda
      tr {x} {y} y∈x x∈col = PT.rec (snd (y ∈ˢ col p)) outer (col-out p x x∈col)
        where
        outer : Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ x)) → ⟨ y ∈ˢ col p ⟩
        outer (r , rp , e) =
          PT.rec (snd (y ∈ˢ col p)) inner
```

Now the chain closes. From `y ∈ col r`, `col-out` applied at `r` yields merely some `s ≺ r` with `col s ≡ y`; call its equation `e2`. Relation transitivity composes `s ≺ r` with `r ≺ p` to give `s ≺ p`, and `col-in p s` promotes `col s` to a member of `col p`. Finally `subst` along `e2` replaces `col s` by `y` in the membership target, delivering `⟨ y ∈ˢ col p ⟩`. Both eliminations of truncation land in the proposition `⟨ y ∈ˢ col p ⟩`, and the whole argument uses only well-founded recursion, transport, and the transitivity hypothesis: no classical principle enters anywhere in this chapter.

```agda
            (col-out r y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x))
          where
          inner : Σ[ s ∈ A ] ((s ≺ r) × (col s ≡ y)) → ⟨ y ∈ˢ col p ⟩
          inner (s , sr , e2) =
            subst (λ v → ⟨ v ∈ˢ col p ⟩) e2 (col-in p s (≺-trans sr rp))
```