An ordinal L-cardinal above every L-cardinal

Given an infinite cardinal of L, this chapter constructs a strictly larger cardinal, represented by an ordinal of L. The construction builds one explicit candidate above the given cardinal; it does not select the least such candidate, which is the task of the later assembly.

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

The base library is opened, and excluded middle is received at the raised level and also lowered to the inner level, where a Bool-valued relation will be decided by it.

open import Base.Prelude
open import Base.Classical using ( LEM; lowerLEM )

The argument is parameterized by excluded middle one universe level above the sets under discussion. Later, the same assumption will be lowered to decide a small proposition when the Hartogs relation is encoded by Booleans. No choice principle is assumed.

module L.CardinalAbove {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

Two properties of the ambient cumulative hierarchy drive the later contradictions. Membership is well-founded, and no set is a member of itself. A presentation supplies indices for a set's members, while self∈sucV places a set in its ordinal successor.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl; regularityV )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}

The constructible side supplies its carrier, transitive constructibility, the ordinal predicate, the stage reading of constructible sets, ordinal facts, and the internal cardinality predicate with its injections.

  using ( 𝒮ʟ; IsOrd; Lset→isL; isTransV; isPropIsTransV )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; boundingOrd )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Cardinal {ℓ} lem using ( IsCardinalL; _↪_ )

Two bridges will connect the construction. The reading lemma turns a coded injection inside L into an actual injection between presentations, and the Mostowski development collapses a transitive well-founded relation to sets. These bridges let an ambient Hartogs argument yield an internal cardinal statement.

open import L.CantorBernstein {ℓ} lem using ( readL )
open import L.Mostowski {ℓ} using ( module Mostowski )

The hierarchy contributes membership bridges, presentations, embedding machinery, the separation construction with its axiom, and the union operation.

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_; sett; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; _∈ₛ_; extensionality; isEmb⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet; module SeparationSet; ⋃_ )

The proof uses ω only in the public statement and uses ordinal successors to create bounds. Sums express the cases of ordinal trichotomy, while Booleans encode the small relation used in the Hartogs construction; the proposition-level lemmas justify the later eliminations from truncated existence.

open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isPropΣ )
open import Cubical.Data.Bool using ( Bool; true; false; false≢true )

Accessibility and well-foundedness, together with the embedding machinery of the cubical library, support the pullback argument of the Hartogs section.

open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded )
open import Cubical.Functions.Embedding
  using ( isEmbedding; injEmbedding; isEmbedding→hasPropFibers
        ; Embedding-into-isSet→isSet )

The empty type refutes impossible cases, and truncated existence is the form in which the chapter's main result is stated.

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )

The ambient and constructible structures are opened as modules, since both are used throughout.

module SV = hPropStructure 𝒮ᵥ
module SL = hPropStructure 𝒮ʟ

The ambient membership is opened under its plain name.

open SV using ( _∈ˢ_ )

Ambient cardinality says that κ admits no injection into the presentation of any member δ ∈ κ. Here an injection is a function equipped with ordinary injectivity, rather than a Cubical embedding record. Ordinality is a separate property and will be proved independently for the candidate constructed below.

IsCardinal : SV.S → Type (ℓ-suc ℓ)
IsCardinal κ = (δ : SV.S) → ⟨ δ ∈ˢ κ ⟩ → (⟪ κ ⟫ ↪ ⟪ δ ⟫ → Empty.⊥)

Injections between types compose by composing the maps and transporting the injectivity proofs through the composite.

comp-inj : {A B C : Type ℓ} → A ↪ B → B ↪ C → A ↪ C
comp-inj (f , injf) (g , injg) =
  (λ x → g (f x)) , λ x y e → injf x y (injg (f x) (f y) e)

If a ∈ b and b is an ordinal, every member of a is also a member of b by transitivity. An index presenting a member of a can therefore be sent to the fiber of the presentation of b over that same set, defining an injection ⟪a⟫ ↪ ⟪b⟫.

ord-emb : (a b : SV.S) → IsOrd b → ⟨ a ∈ˢ b ⟩ → ⟪ a ⟫ ↪ ⟪ b ⟫
ord-emb a b ob a∈b = f , inj
  where
  f : ⟪ a ⟫ → ⟪ b ⟫
  f m = fiber b {x = ⟪ a ⟫↪ m} (ob .fst (member a m) a∈b) .fst

The embedding is injective, because the fiber identifications of two indices are chained through the equality of their images.

  inj : (m n : ⟪ a ⟫) → f m ≡ f n → m ≡ n
  inj m n e = ↪-inj {a = a}
    (sym (fiber b {x = ⟪ a ⟫↪ m} (ob .fst (member a m) a∈b) .snd)
      ∙ cong (⟪ b ⟫↪) e
      ∙ fiber b {x = ⟪ a ⟫↪ n} (ob .fst (member a n) a∈b) .snd)

The target statement

The public goal takes a constructible κ, together with proofs that its underlying set is an ordinal, is an internal cardinal, and is not a member of ω. It asks only for the propositionally truncated existence of a constructible θ; no particular witness may be extracted from the theorem.

CardAboveLᵀ : Type (ℓ-suc ℓ)
CardAboveLᵀ =
    (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ
  → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → ∥ Σ[ θ ∈ SL.S ]

The produced θ must be an ordinal, an internal cardinal, and strictly above κ, the last membership expressing the strict inequality of von Neumann ordinals.

       (IsOrd (fst θ) × IsCardinalL θ × ⟨ fst κ ∈ˢ fst θ ⟩) ∥₁

Ordinals as elements of L

An ambient ordinal becomes an element of L by being presented at its own successor stage: the stage Lset (sucV x) contains x, is indexed by an ordinal, and carries the constructibility of x. This is a natural representative; the chapter does not claim it to be the earliest stage containing x.

ordL : (x : SV.S) → IsOrd x → SL.S
ordL x ox = x , Lset→isL (sucV x) (suc-ord ox) x (ord∈Lset-suc x ox)

From ambient to internal cardinality

Ambient cardinality implies internal cardinality, in one direction only. A coded injection is read as an ambient injection by its own reading lemma, so the ambient refutation eliminates the truncated coding; the elimination is legitimate because the target is the empty type.

ambient→internal : (κ : SL.S) → IsCardinal (fst κ) → IsCardinalL κ
ambient→internal κ c δ δ∈κ h =
  PT.rec Empty.isProp⊥ (λ w → c (fst δ) δ∈κ (readL κ δ w)) h

Separating smaller cardinals

Fix a set a and an ordinal bound β. The construction separates from β those members whose presentations inject into the presentation of a. In the later application a is also an ordinal, but only the ordinality of the bound is needed inside this module.

module Sep (a : SV.S) (β : SV.S) (oβ : IsOrd β) where

The separating predicate asks whether a set embeds into a, and is stated as a truncated existence. Since it lives in hProp ℓ by construction, it can be handed to separation directly, with no resizing step in between.

  ϕ : SV.S → hProp ℓ
  ϕ x = ∥ ⟪ x ⟫ ↪ ⟪ a ⟫ ∥₁ , squash₁

The separation construction of the hierarchy is opened at the ordinal bound with this predicate.

  open SeparationSet β ϕ using ( SEPAREE; separation-ax )

The separated set is named θ: it collects exactly those members of the bound that embed into a.

  θ : SV.S
  θ = SEPAREE

Membership in θ is introduced from membership in the bound together with a truncated embedding into a, through the separation axiom.

  θ-in : (x : SV.S) → ⟨ x ∈ˢ β ⟩ → ∥ ⟪ x ⟫ ↪ ⟪ a ⟫ ∥₁ → ⟨ x ∈ˢ θ ⟩
  θ-in x x∈β h =
    ∈∈ₛ {a = x} {b = θ} .snd
      (separation-ax x .snd (∈∈ₛ {a = x} {b = β} .fst x∈β , h))

Conversely, membership in θ forgets the separating condition and keeps only membership in the bound.

  θ⊆β : (x : SV.S) → ⟨ x ∈ˢ θ ⟩ → ⟨ x ∈ˢ β ⟩
  θ⊆β x x∈θ =
    ∈∈ₛ {a = x} {b = β} .snd
      (separation-ax x .fst (∈∈ₛ {a = x} {b = θ} .fst x∈θ) .fst)

The separating condition is recovered only as a truncated existence of an embedding; no concrete embedding is selected from it.

  θ-inj : (x : SV.S) → ⟨ x ∈ˢ θ ⟩ → ∥ ⟪ x ⟫ ↪ ⟪ a ⟫ ∥₁
  θ-inj x x∈θ = separation-ax x .fst (∈∈ₛ {a = x} {b = θ} .fst x∈θ) .snd

The separated set θ is an ordinal. Its transitivity is proved below. Each of its members is transitive because it is also a member of the ordinal β; together these are the two parts of IsOrd θ.

  θ-ord : IsOrd θ
  θ-ord = trans , (λ x x∈θ → oβ .snd x (θ⊆β x x∈θ))
    where
    trans : isTransV θ
    trans {x} {y} y∈x x∈θ =

To prove transitivity, take y ∈ x ∈ θ. Since x is a member of the ordinal bound, it is itself an ordinal, so membership gives an injection from y into x. Composing this with the merely existing injection from x into a yields the merely existing injection from y into a; transitivity of the bound also gives y ∈ β, so θ-in returns y ∈ θ.

      θ-in y (oβ .fst y∈x (θ⊆β x x∈θ))
        (PT.map
          (comp-inj (ord-emb y x (mem-ord {A = β} oβ x (θ⊆β x x∈θ)) y∈x))
          (θ-inj x x∈θ))

The parameter a itself belongs to θ as soon as it belongs to the bound: the identity map witnesses its embedding into itself.

  a∈θ : ⟨ a ∈ˢ β ⟩ → ⟨ a ∈ˢ θ ⟩
  a∈θ a∈β = θ-in a a∈β ∣ (λ m → m) , (λ m n e → e) ∣₁

Assume now that θ ∈ β. If θ injected into some δ ∈ θ, the separating condition for δ would merely supply an injection δ ↪ a. Composing inside the truncation gives an injection θ ↪ a; together with θ ∈ β, the separation rule would then place θ in itself, contradicting irreflexivity. Thus θ is an ambient cardinal.

  θ-card : ⟨ θ ∈ˢ β ⟩ → IsCardinal θ
  θ-card θ∈β δ δ∈θ f =
    ∈-irrefl θ (θ-in θ θ∈β (PT.map (comp-inj f) (θ-inj δ δ∈θ)))

It remains to prove θ ∈ β, and one ordinal γ ∈ β with no injection into a is enough. Trichotomy compares the two ordinals θ and β; the next clauses eliminate equality and the case in which β lies below θ.

  θ∈β : (γ : SV.S) → ⟨ γ ∈ˢ β ⟩ → (⟪ γ ⟫ ↪ ⟪ a ⟫ → Empty.⊥)
      → ⟨ θ ∈ˢ β ⟩
  θ∈β γ γ∈β noinj = go (ord-tri θ θ-ord β oβ)
    where
    go : Tri θ β → ⟨ θ ∈ˢ β ⟩

Trichotomy leaves only θ ∈ β. That case gives the result directly. If θ ≡ β, transporting γ ∈ β makes γ a member of θ; its separating condition then contradicts the assumed absence of an injection γ ↪ a. If β ∈ θ, the inclusion θ ⊆ β gives β ∈ β, again a contradiction. This locates θ below the chosen bound without asserting that it is the least ordinal with any property.

    go (inl θ∈β')      = θ∈β'
    go (inr (inl e))   =
      Empty.rec (PT.rec Empty.isProp⊥ noinj
        (θ-inj γ (subst (λ v → ⟨ γ ∈ˢ v ⟩) (sym e) γ∈β)))
    go (inr (inr β∈θ)) = Empty.rec (∈-irrefl β (θ⊆β β β∈θ))

Reducing to an ambient bound

The Hartogs input is stated in its weakest form: for every ordinal, some ordinal does not inject into it. No constructibility, no coding, and no leastness is carried by this type; the truncated existential names an ordinal and its non-injectivity alone.

NoInjOrd : Type (ℓ-suc ℓ)
NoInjOrd = (x : SV.S) → IsOrd x
         → ∥ Σ[ γ ∈ SV.S ] (IsOrd γ × (⟪ γ ⟫ ↪ ⟪ x ⟫ → Empty.⊥)) ∥₁

The positional lemma compares two ordinals and concludes that the first belongs to the second. Trichotomy decides three cases, and two of them are contradictory.

above : (a γ : SV.S) → IsOrd a → IsOrd γ → (⟪ γ ⟫ ↪ ⟪ a ⟫ → Empty.⊥)
      → ⟨ a ∈ˢ γ ⟩
above a γ oa oγ noinj = go (ord-tri γ oγ a oa)
  where
  idInj : ⟪ γ ⟫ ↪ ⟪ γ ⟫

The identity injection of the ordinal into itself is named first. If the second ordinal were below the first, or equal to it, the transported injection would contradict the non-injectivity hypothesis.

  idInj = (λ m → m) , (λ m n e → e)
  go : Tri γ a → ⟨ a ∈ˢ γ ⟩
  go (inl γ∈a)      = Empty.rec (noinj (ord-emb γ a oa γ∈a))
  go (inr (inl e))  =
    Empty.rec (noinj (subst (λ v → ⟪ γ ⟫ ↪ ⟪ v ⟫) e idInj))

Only the third case of the trichotomy survives, which is the announced membership.

  go (inr (inr a∈γ)) = a∈γ

Suppose an explicit ordinal γ with no injection into a has been given. The separated set formed from this witness is explicitly available and is proved to be an ordinal, an ambient cardinal, and strictly above a. The surrounding existence claim may still be truncated; this lemma itself maps an unpacked witness to an unpacked result.

cardAboveAt : (a : SV.S) → IsOrd a
  → Σ[ γ ∈ SV.S ] (IsOrd γ × (⟪ γ ⟫ ↪ ⟪ a ⟫ → Empty.⊥))
  → Σ[ θ ∈ SV.S ] (IsOrd θ × IsCardinal θ × ⟨ a ∈ˢ θ ⟩)
cardAboveAt a oa (γ , oγ , noinj) =
  S.θ , S.θ-ord , S.θ-card θ∈sγ , S.a∈θ a∈sγ

Use the ordinal successor sucV γ as the bound for separation. The witness lies in its own successor. The lemma above gives a ∈ γ, and transitivity of the successor ordinal then also places a inside the bound.

  where
  module S = Sep a (sucV γ) (suc-ord oγ)
  γ∈sγ : ⟨ γ ∈ˢ sucV γ ⟩
  γ∈sγ = self∈sucV γ
  a∈sγ : ⟨ a ∈ˢ sucV γ ⟩

The two needed side conditions now follow. From a ∈ γ ∈ sucV γ we obtain a ∈ sucV γ, so the identity injection places a in the separated set. The witness γ ∈ sucV γ and its failure to inject into a force the separated set itself to lie below the bound, enabling the cardinal proof.

  a∈sγ = suc-ord oγ .fst (above a γ oa oγ noinj) γ∈sγ
  θ∈sγ : ⟨ S.θ ∈ˢ sucV γ ⟩
  θ∈sγ = S.θ∈β γ γ∈sγ noinj

The ambient existence theorem restores the truncation: from the Hartogs input, which supplies a witness for every ordinal, it produces, for the given ordinal a, the truncated ambient cardinal above it.

ambientCardAbove : NoInjOrd → (a : SV.S) → IsOrd a
  → ∥ Σ[ θ ∈ SV.S ] (IsOrd θ × IsCardinal θ × ⟨ a ∈ˢ θ ⟩) ∥₁
ambientCardAbove ni a oa = PT.map (cardAboveAt a oa) (ni a oa)

The ambient existence theorem is now transferred to L. Of the three mathematical hypotheses on κ, this construction uses its ordinality to invoke the ambient theorem. Its internal cardinality and its being outside ω are stronger assumptions of the stated result, appropriate to the later application to infinite cardinals, but no step of this existence proof consumes them.

noInjOrd→CardAboveLᵀ : NoInjOrd → CardAboveLᵀ
noInjOrd→CardAboveLᵀ ni κ oκ cκ κ∉ω =
  PT.map build (ambientCardAbove ni (fst κ) oκ)
  where
  build : Σ[ θ ∈ SV.S ] (IsOrd θ × IsCardinal θ × ⟨ fst κ ∈ˢ θ ⟩)

The ambient cardinal is presented as an element of L at its own successor stage, its cardinality is transported into the internal predicate by the one-directional comparison, and the membership of κ below it passes through unchanged.

        → Σ[ θ ∈ SL.S ]
            (IsOrd (fst θ) × IsCardinalL θ × ⟨ fst κ ∈ˢ fst θ ⟩)
  build (θ , oθ , cθ , κ∈θ) =
    ordL θ oθ , oθ , ambient→internal (ordL θ oθ) cθ , κ∈θ

The Hartogs ordinal

The Hartogs construction is organized in a module over an arbitrary ambient set a. It produces an ordinal that cannot inject into a without assuming that a is itself an ordinal; ordinality is required only later, when non-injectivity is converted into the strict comparison a ∈ γ.

module Hartogs (a : SV.S) where

A relation on the presentation of a is a Boolean-valued function of two arguments.

  Rel : Type ℓ
  Rel = ⟪ a ⟫ → ⟪ a ⟫ → Bool

A Boolean relation holds of two arguments when its value is the Boolean true; the reading is a proposition, since Booleans form a set.

  Holds : Rel → ⟪ a ⟫ → ⟪ a ⟫ → Type ℓ-zero
  Holds R x y = R x y ≡ true

A well-founded relation on the presentation of a is a Boolean relation that is transitive and well-founded. It is not required to be linear or trichotomous, so a member of this type is not yet a well order.

  WFR : Type ℓ
  WFR = Σ[ R ∈ Rel ]
          ( ({x y z : ⟪ a ⟫} → Holds R x y → Holds R y z → Holds R x z)
          × WellFounded (λ x y → Holds R x y) )

Each well-founded Boolean relation is given its own collapse module.

  module Col (w : WFR) where

Fix one such relation w. Its first component is the Boolean relation R; the remaining components certify transitivity and well-foundedness. The collapse argument keeps these roles separate because the relation determines membership, while the proofs justify recursion and ordinal transitivity.

    R : Rel
    R = fst w

On the collapsed side, the relation is read through a lifted form of the Boolean holds, so that it lives at the level the Mostowski development expects.

    _≺_ : ⟪ a ⟫ → ⟪ a ⟫ → Type ℓ
    x ≺ y = Lift (Holds R x y)

The lifted relation inherits transitivity from the original Bool-valued relation. Lowering the two lifted hypotheses exposes Boolean equalities that can be composed by the transitivity stored in w, and lifting the result returns it at the universe level required by the collapse.

    ≺-trans : {x y z : ⟪ a ⟫} → x ≺ y → y ≺ z → x ≺ z
    ≺-trans p q = lift (fst (snd w) (lower p) (lower q))

Well-foundedness is preserved by the same change of universe. Starting from the accessibility tree for the Bool-valued relation, go recursively replaces every predecessor edge by its lifted counterpart, producing an accessibility tree for _≺_.

    ≺-wf : WellFounded _≺_
    ≺-wf x = go x (snd (snd w) x)
      where
      go : (y : ⟪ a ⟫) → Acc (λ u v → Holds R u v) y → Acc _≺_ y
      go y (acc h) = acc (λ z k → go z (h z (lower k)))

The lifted relation now meets the two hypotheses of the Mostowski construction: it is transitive and well founded. We may therefore use its collapse col; the accompanying laws describe membership in each collapse value and prove that every such value is an ordinal.

    open Mostowski ⟪ a ⟫ _≺_ ≺-wf ≺-trans public
      using ( col; col-eq; col-in; col-out; col-ord )

Collect all collapse values into their image ot. Although the name suggests an order type, an arbitrary member of WFR need not be a well order, and no uniqueness or isomorphism theorem is asserted here. What matters is simply that this image can be proved to be an ordinal.

    ot : SV.S
    ot = sett ⟪ a ⟫ col

Each col p belongs to the image. The displayed witness is the index p together with reflexivity, wrapped in propositional truncation because membership in an image remembers only that some preimage exists.

    ot-in : (p : ⟪ a ⟫) → ⟨ col p ∈ˢ ot ⟩
    ot-in p = ∣ p , refl ∣₁

The image is an ordinal. First, a member of the image is merely equal to some collapse value, hence is transitive because that collapse value is an ordinal. Second, the image itself is transitive: if y ∈ x and x is represented by col p, col-out merely presents y as col r for a predecessor r; the canonical image witness for r then puts y in ot. Both truncated existences are eliminated only into proposition-valued membership or transitivity goals.

    ot-ord : IsOrd ot
    ot-ord = tr , mem
      where
      mem : (x : SV.S) → ⟨ x ∈ˢ ot ⟩ → isTransV x
      mem x x∈ = PT.rec (isPropIsTransV x)

The member's transitivity is transported from the collapse's ordinality along the presentation equation, and the outer elimination consumes the truncated decomposition of the member inside the image.

        (λ z → subst isTransV (snd z) (col-ord (fst z) .fst)) x∈
      tr : isTransV ot
      tr {x} {y} y∈x x∈ot = PT.rec (snd (y ∈ˢ ot)) outer x∈ot
        where
        outer : Σ[ p ∈ ⟪ a ⟫ ] (col p ≡ x) → ⟨ y ∈ˢ ot ⟩

The truncated decomposition names an index r whose collapse is y and proves that r precedes p. The collapse law places col r in col p, while the canonical image witness ot-in r places col r in ot. Transport along the equation col r ≡ y therefore gives y ∈ ot.

        outer (p , e) =
          PT.rec (snd (y ∈ˢ ot))
            (λ z → subst (λ v → ⟨ v ∈ˢ ot ⟩) (snd (snd z)) (ot-in (fst z)))
            (col-out p y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x))

The Hartogs candidate μ is the union of the successors of all collapse images arising from WFR. Including each successor, rather than only the image itself, ensures that every Col.ot w is a strict member of the common bound. This construction bounds all such images without claiming that any of them is a uniquely determined order type.

  μ : SV.S
  μ = ⋃ (sett WFR (λ w → sucV (Col.ot w)))

The bounding ordinal is an ordinal, proved by the bounding lemma from the fact that every member of the family is itself an ordinal.

  μ-ord : IsOrd μ
  μ-ord = boundingOrd WFR Col.ot Col.ot-ord .snd .fst

For every w : WFR, its collapse image Col.ot w is a member of μ. This strict bound is the half of the final contradiction supplied in advance: once the opposite inclusion μ ⊆ Col.ot w is obtained for a relation pulled back from a hypothetical injection, self-membership follows.

  ot∈μ : (w : WFR) → ⟨ Col.ot w ∈ˢ μ ⟩
  ot∈μ = boundingOrd WFR Col.ot Col.ot-ord .snd .snd

For any set x in the ambient cumulative hierarchy, its presentation type ⟪ x ⟫ embeds into the hierarchy itself. Since the hierarchy is an h-set, the presentation type is also an h-set. This lets ordinary injectivity into ⟪ a ⟫ be upgraded to proposition-valued fibres.

  isSet⟪⟫ : (x : SV.S) → isSet ⟪ x ⟫
  isSet⟪⟫ x = Embedding-into-isSet→isSet (⟪ x ⟫↪ , isEmb⟪ x ⟫↪) setIsSet

The decider converts a classical case split into a Boolean value, encoding the two branches as true and false.

  decB : {A : Type ℓ} → (A ⊎ (A → Empty.⊥)) → Bool
  decB (inl _) = true
  decB (inr _) = false

The excluded-middle instance is lowered from the successor level to the working level, so that propositions living at the working level can be decided.

  lemℓ : LEM ℓ
  lemℓ = lowerLEM lem

Assume for contradiction an injection f : ⟪ μ ⟫ ↪ ⟪ a ⟫. The next construction transports membership among the presented members of μ to the image of this injection, producing one of the relations already included in the family WFR.

  module NoInj (f : ⟪ μ ⟫ ↪ ⟪ a ⟫) where

The underlying function of the embedding is named once for the subsequent constructions.

    F : ⟪ μ ⟫ → ⟪ a ⟫
    F = fst f

Because both the source and the target are h-sets, the injective function is an embedding: each fibre is a proposition.

    F-emb : isEmbedding F
    F-emb = injEmbedding (isSet⟪⟫ a) (λ {x} {y} e → snd f x y e)

The fibre over a point consists of an index of a member of μ together with an equation saying that F maps that index to the point. Thus an inhabitant of Fib x is precisely a presentation of x as lying in the image of F.

    Fib : ⟪ a ⟫ → Type ℓ
    Fib x = Σ[ m ∈ ⟪ μ ⟫ ] (F m ≡ x)

Every fibre of F is a proposition. Consequently, whenever two pulled-back relation proofs present the same image point by possibly different indices, those fibre elements are equal. This uniqueness aligns their representatives; it does not choose a representative for points outside the image.

    isPropFib : (x : ⟪ a ⟫) → isProp (Fib x)
    isPropFib = isEmbedding→hasPropFibers F-emb

The relation PreT x y first requires actual fibres witnessing that both x and y lie in the image of F. It then declares x to precede y exactly when the corresponding presented members of μ stand in the small membership relation. Points outside the image therefore have no predecessors in this relation.

    PreT : ⟪ a ⟫ → ⟪ a ⟫ → Type ℓ
    PreT x y = Σ[ p ∈ Fib x ] Σ[ q ∈ Fib y ]
                 ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst q) ⟩

The pulled-back predecessor relation is a proposition: it is built from two proposition fibres and one membership proposition.

    isPropPreT : (x y : ⟪ a ⟫) → isProp (PreT x y)
    isPropPreT x y = isPropΣ (isPropFib x) λ p →
                     isPropΣ (isPropFib y) λ q →
                       snd (⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst q))

The Bool relation is the decidable encoding of the pulled-back predecessor relation, obtained by applying excluded middle to the proposition-valued relation.

    R : Rel
    R x y = decB (lemℓ (PreT x y , isPropPreT x y))

If the Boolean relation holds, its value is true. Inspecting the excluded-middle decision then recovers PreT x y: the positive branch contains the desired proof, while the negative branch would force the Boolean value to be false and is therefore contradictory.

    R→Pre : (x y : ⟪ a ⟫) → Holds R x y → PreT x y
    R→Pre x y e = go (lemℓ (PreT x y , isPropPreT x y)) e
      where
      go : (d : PreT x y ⊎ (PreT x y → Empty.⊥)) → decB d ≡ true → PreT x y
      go (inl h) _  = h

The refutation branch is impossible: if the predecessor fact does not hold, the decider would have returned false, contradicting the true membership.

      go (inr _) e' = Empty.rec (false≢true e')

The backward reading constructs the Boolean membership from the pulled-back predecessor fact, by the same classical decision.

    Pre→R : (x y : ⟪ a ⟫) → PreT x y → Holds R x y
    Pre→R x y h = go (lemℓ (PreT x y , isPropPreT x y))
      where
      go : (d : PreT x y ⊎ (PreT x y → Empty.⊥)) → decB d ≡ true
      go (inl _) = refl

The empty branch is impossible: the predecessor fact holds by assumption.

      go (inr n) = Empty.rec (n h)

To prove transitivity, decode x R y and y R z into two PreT witnesses. They contain four fibre witnesses: one over x, two over the shared middle point y, and one over z. Since the fibre over y is a proposition, its two witnesses are equal, so the corresponding members of μ can be aligned. Transitivity of the final represented member then composes the two membership steps, producing a PreT witness for x R z.

    R-trans : {x y z : ⟪ a ⟫} → Holds R x y → Holds R y z → Holds R x z
    R-trans {x} {y} {z} e1 e2 = Pre→R x z (p , r , goal)
      where
      d1 : PreT x y
      d1 = R→Pre x y e1

Decoding the first relation gives indices p and q over x and y; decoding the second gives q' and r over y and z. Propositionality of the fibre over y identifies q with q', allowing the membership represented by the first relation to be rewritten with the same middle index as the second.

      d2 : PreT y z
      d2 = R→Pre y z e2
      p  = fst d1
      q  = fst (snd d1)
      q' = fst d2

The final member r is named, and its transitivity is read from the ordinality of μ.

      r  = fst (snd d2)
      h1' : ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst q') ⟩
      h1' = subst (λ t → ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst t) ⟩)
              (isPropFib y q q') (snd (snd d1))
      rTr : isTransV (⟪ μ ⟫↪ (fst r))

The composition of the two membership relations through the transitivity of r produces the goal: the first member is inside the third member, which is what the pulled-back relation requires.

      rTr = μ-ord .snd (⟪ μ ⟫↪ (fst r)) (member μ (fst r))
      goal : ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst r) ⟩
      goal = ∈∈ₛ {a = ⟪ μ ⟫↪ (fst p)} {b = ⟪ μ ⟫↪ (fst r)} .fst
        (rTr (∈∈ₛ {a = ⟪ μ ⟫↪ (fst p)} {b = ⟪ μ ⟫↪ (fst q')} .snd h1')
             (∈∈ₛ {a = ⟪ μ ⟫↪ (fst q')} {b = ⟪ μ ⟫↪ (fst r)} .snd (snd (snd d2))))

Well-foundedness is transported along the injection from the ambient hierarchy's regularity. The auxiliary lemma handles the case where the target is known to equal a specific hierarchy element.

The auxiliary proof constructs accessibility for each predecessor of the given member.

    wfAux : (v : SV.S) → Acc SV._∈ᵗ_ v → (m : ⟪ μ ⟫) → ⟪ μ ⟫↪ m ≡ v
          → Acc (λ x y → Holds R x y) (F m)
    wfAux v (acc rec) m e = acc go
      where
      go : (r : ⟪ a ⟫) → Holds R r (F m) → Acc (λ x y → Holds R x y) r

Each predecessor r of the member is decomposed into two μ members connected by the pulled-back relation, and the accessibility is transported to the first component.

      go r rr = subst (Acc (λ x y → Holds R x y)) (snd p)
                  (wfAux (⟪ μ ⟫↪ (fst p)) (rec (⟪ μ ⟫↪ (fst p)) below)
                     (fst p) refl)
        where
        d : PreT r (F m)

The predecessor fact is decomposed to name two internal indices: p presents the predecessor r inside μ, and q presents the target F m inside μ. The transported equation identifies the two presentations of the middle member.

        d = R→Pre r (F m) rr
        p = fst d
        q = fst (snd d)
        h : ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ m ⟩
        h = subst (λ t → ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst t) ⟩)

The two fibre witnesses over F m are equal because that fibre is a proposition. Transporting along this equality rewrites the decoded relation as membership of the predecessor represented by p in the member represented by m. The equation identifying that latter member with v then places the predecessor strictly below v, where the accessibility recursion applies.

              (isPropFib (F m) q (m , refl)) (snd (snd d))
        below : ⟪ μ ⟫↪ (fst p) SV.∈ᵗ v
        below = subst (λ t → ⟨ ⟪ μ ⟫↪ (fst p) ∈ˢ t ⟩) e
                  (∈∈ₛ {a = ⟪ μ ⟫↪ (fst p)} {b = ⟪ μ ⟫↪ m} .snd h)

Well-foundedness of the pulled-back relation follows from the regularity of the ambient hierarchy: each predecessor of any member lies strictly below some hierarchy element, and the auxiliary lemma produces accessibility there.

    R-wf : WellFounded (λ x y → Holds R x y)
    R-wf x = acc go
      where
      go : (r : ⟪ a ⟫) → Holds R r x → Acc (λ u v → Holds R u v) r
      go r rr = subst (Acc (λ u v → Holds R u v)) (snd p)

For an arbitrary predecessor r of x, decoding the relation supplies a fibre witness p over r. Regularity gives accessibility of the hierarchy element represented by its index, and wfAux transfers that accessibility back to the point F (fst p). The fibre equation identifies this point with r, completing the required accessibility proof.

                  (wfAux (⟪ μ ⟫↪ (fst p)) (regularityV (⟪ μ ⟫↪ (fst p)))
                     (fst p) refl)
        where
        p = fst (R→Pre r x rr)

The well-founded transitive relation is packaged with its two proofs, completing the well-founded relation family that the bounding ordinal ranges over.

    w : WFR
    w = R , R-trans , R-wf

Apply the collapse construction to the particular relation w obtained from the hypothetical injection. Its collapse values and their image will now be compared directly with the presented members of μ; no claim that w is a well order is needed.

    open Col w using ( col; col-in; col-out; ot; ot-in; _≺_ )

The key lemma says that the collapse of the pullback relation reproduces the members of the bounding ordinal: for each μ member presented as a hierarchy element, the collapse of its image equals that element. The proof is by well-founded induction on the hierarchy element.

The proof compares members by extensionality in two directions.

    key : (v : SV.S) → Acc SV._∈ᵗ_ v → (m : ⟪ μ ⟫) → ⟪ μ ⟫↪ m ≡ v
        → col (F m) ≡ ⟪ μ ⟫↪ m
    key v (acc rec) m e =
      extensionality (col (F m)) (⟪ μ ⟫↪ m) (fwd , bwd)
      where

For the forward inclusion, suppose b belongs to col (F m). The elimination law col-out says merely that b is the collapse of some predecessor r of F m. Decoding that predecessor through PreT reveals an index below m; the induction hypothesis will identify its represented member with col r and hence with b.

      fwd : (b : SV.S) → ⟨ b ∈ₛ col (F m) ⟩ → ⟨ b ∈ₛ ⟪ μ ⟫↪ m ⟩
      fwd b b∈ = PT.rec (snd (b ∈ₛ ⟪ μ ⟫↪ m)) go
                   (col-out (F m) b (∈∈ₛ {a = b} {b = col (F m)} .snd b∈))
        where
        go : Σ[ r ∈ ⟪ a ⟫ ] ((r ≺ F m) × (col r ≡ b))

The predecessor witness consists of r ≺ F m and an equation col r ≡ b. Reading the relation proof back through R→Pre yields fibres for r and F m; their indices identify the corresponding presented members of μ, while the final component records membership between them.

           → ⟨ b ∈ₛ ⟪ μ ⟫↪ m ⟩
        go (r , rr , cr) = subst (λ t → ⟨ t ∈ₛ ⟪ μ ⟫↪ m ⟩) (cpr ∙ cr) hh
          where
          d = R→Pre r (F m) (lower rr)
          p = fst d

The fibre over F m is proposition-valued, so the representative q obtained from the relation proof equals the evident representative (m , refl). Transport along this equality turns the decoded membership into the statement that the predecessor index lies inside the set represented by m.

          q = fst (snd d)
          hh : ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ m ⟩
          hh = subst (λ t → ⟨ ⟪ μ ⟫↪ (fst p) ∈ₛ ⟪ μ ⟫↪ (fst t) ⟩)
                 (isPropFib (F m) q (m , refl)) (snd (snd d))
          below : ⟪ μ ⟫↪ (fst p) SV.∈ᵗ v

Using the equation ⟪ μ ⟫↪ m ≡ v, this membership places the predecessor's represented set below v in ambient membership. The recursive hypothesis is therefore available at that predecessor and identifies its collapse with its represented set.

          below = subst (λ t → ⟨ ⟪ μ ⟫↪ (fst p) ∈ˢ t ⟩) e
                    (∈∈ₛ {a = ⟪ μ ⟫↪ (fst p)} {b = ⟪ μ ⟫↪ m} .snd hh)
          ih : col (F (fst p)) ≡ ⟪ μ ⟫↪ (fst p)
          ih = key (⟪ μ ⟫↪ (fst p)) (rec (⟪ μ ⟫↪ (fst p)) below) (fst p) refl
          cpr : ⟪ μ ⟫↪ (fst p) ≡ col r

The induction hypothesis identifies the collapse of the decoded index with the member represented by that index. Since the fibre equation also identifies its image with r, congruence of col yields the required equation between the represented member and col r; composing with col r ≡ b completes the forward inclusion.

          cpr = sym ih ∙ cong col (snd p)

For the reverse inclusion, begin with b as a member of the set represented by m. The aim is to exhibit b as a member of col (F m). Transitivity of the ordinal μ first promotes b to membership in μ, allowing its canonical presentation to supply an index k for b.

      bwd : (b : SV.S) → ⟨ b ∈ₛ ⟪ μ ⟫↪ m ⟩ → ⟨ b ∈ₛ col (F m) ⟩
      bwd b b∈ = ∈∈ₛ {a = b} {b = col (F m)} .fst
                   (subst (λ t → ⟨ t ∈ˢ col (F m) ⟩) (ihk ∙ ek) inCol)
        where
        b∈ˢ : ⟨ b ∈ˢ ⟪ μ ⟫↪ m ⟩

Here fiber μ b∈μ returns an actual index k and an equation ⟪ μ ⟫↪ k ≡ b. This is possible because small membership _∈ₛ_ is based on the proposition-valued fibre of the canonical presentation. It is a local inverse to that presentation, not a choice from an arbitrary truncated existence.

        b∈ˢ = ∈∈ₛ {a = b} {b = ⟪ μ ⟫↪ m} .snd b∈
        b∈μ : ⟨ b ∈ˢ μ ⟩
        b∈μ = μ-ord .fst b∈ˢ (member μ m)
        fb = fiber μ b∈μ
        k = fst fb

The equation returned by fiber lets us rewrite the original membership b ∈ ⟪ μ ⟫↪ m as membership of the represented element ⟪ μ ⟫↪ k. The evident fibres (k , refl) and (m , refl), together with this membership, then establish PreT (F k) (F m).

        ek : ⟪ μ ⟫↪ k ≡ b
        ek = snd fb
        k∈m : ⟨ ⟪ μ ⟫↪ k ∈ₛ ⟪ μ ⟫↪ m ⟩
        k∈m = subst (λ t → ⟨ t ∈ₛ ⟪ μ ⟫↪ m ⟩) (sym ek) b∈
        pre : PreT (F k) (F m)

Encoding this PreT fact as the Bool relation gives F k ≺ F m. The collapse introduction law therefore places col (F k) inside col (F m). At the same time, the membership of the represented element below m places it below the induction parameter v, so the recursive hypothesis applies to k.

        pre = (k , refl) , ((m , refl) , k∈m)
        inCol : ⟨ col (F k) ∈ˢ col (F m) ⟩
        inCol = col-in (F m) (F k) (lift (Pre→R (F k) (F m) pre))
        below : ⟪ μ ⟫↪ k SV.∈ᵗ v
        below = subst (λ t → ⟨ ⟪ μ ⟫↪ k ∈ˢ t ⟩) e

The recursive hypothesis gives col (F k) ≡ ⟪ μ ⟫↪ k. Composing this with the fibre equation ⟪ μ ⟫↪ k ≡ b transports the membership just constructed to b ∈ col (F m), completing the reverse inclusion.

                  (∈∈ₛ {a = ⟪ μ ⟫↪ k} {b = ⟪ μ ⟫↪ m} .snd k∈m)
        ihk : col (F k) ≡ ⟪ μ ⟫↪ k
        ihk = key (⟪ μ ⟫↪ k) (rec (⟪ μ ⟫↪ k) below) k refl

Regularity supplies the accessibility proof needed to specialize the induction to every index m of μ. Thus key' identifies col (F m) with the member represented by m. The next part of the proof will use these pointwise equalities to establish the inclusion μ ⊆ Col.ot w; that inclusion has not yet been asserted here.

    key' : (m : ⟪ μ ⟫) → col (F m) ≡ ⟪ μ ⟫↪ m
    key' m = key (⟪ μ ⟫↪ m) (regularityV (⟪ μ ⟫↪ m)) m refl

Every member b of μ also belongs to the collapse image ot. The canonical fibre of μ at b supplies an index m with ⟪ μ ⟫↪ m ≡ b. The lemma key' identifies that representative with col (F m), while ot-in places this collapse value in ot; transport along the two equalities yields b ∈ ot.

Thus the argument establishes only the inclusion μ ⊆ ot. Together with ot ∈ μ, this inclusion will already be enough for the contradiction, so no equality or order isomorphism between μ and ot is required.

    μ⊆ot : (b : SV.S) → ⟨ b ∈ˢ μ ⟩ → ⟨ b ∈ˢ ot ⟩
    μ⊆ot b b∈μ =
      subst (λ t → ⟨ t ∈ˢ ot ⟩) (key' (fst fb) ∙ snd fb)
        (ot-in (F (fst fb)))
      where

The canonical presentation has proposition-valued fibres, so the representative recovered for b is uniquely determined. Keeping that representative and its equation together as fb supplies exactly the index used by both key' and ot-in in the preceding inclusion proof.

      fb = fiber μ b∈μ

By construction of the bound, ot is a member of μ. Applying the inclusion μ ⊆ ot to that particular member gives ot ∈ ot, contradicting the irreflexivity of membership. This closes the contradiction generated by the assumed injection μ ↪ a.

    absurd : Empty.⊥
    absurd = ∈-irrefl ot (μ⊆ot ot (ot∈μ w))

The local contradiction was proved under an arbitrary injection f : ⟪ μ ⟫ ↪ ⟪ a ⟫. The theorem noInj now exposes that conclusion at the boundary of the Hartogs module: every proposed injection supplies the pullback relation above and therefore leads to Empty.⊥.

  noInj : (⟪ μ ⟫ ↪ ⟪ a ⟫) → Empty.⊥
  noInj f = NoInj.absurd f

The larger L-cardinal

For each ordinal x, the explicit object Hartogs.μ x is an ordinal and admits no injection into x. These three pieces are then placed under propositional truncation to satisfy NoInjOrd. The construction therefore provides a definite witness before packaging it, while callers receive only its truncated existence.

noInjOrd : NoInjOrd
noInjOrd x ox = ∣ Hartogs.μ x , Hartogs.μ-ord x , Hartogs.noInj x ∣₁

Finally, noInjOrd→CardAboveLᵀ turns the Hartogs witness into a strictly larger ambient ordinal cardinal, places that ordinal in L, and transfers its ambient cardinality to internal cardinality. The result is propositionally truncated: for the given ordinal cardinal κ, some constructible internal cardinal θ satisfies κ ∈ θ.

This theorem supplies the nonempty collection needed for the later successor-cardinal construction. It does not choose its least member; L.GCH.Assembly performs that minimisation after using this witness to bound the search.

CardAboveL : CardAboveLᵀ
CardAboveL = noInjOrd→CardAboveLᵀ noInjOrd