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.

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

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.

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.

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.

  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.

    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.

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

  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.

      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.

      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.

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