---
title: "Choosing a cardinal representative for an ordinal"
module: L.GCH.CardinalRepresentative
lang: en
site: "Bedrock"
description: "Choosing a cardinal representative for an ordinal"
stage: "Proving GCH"
reading_order: 110
canonical: https://bedrock.institute/en/L.GCH.CardinalRepresentative.html
html: L.GCH.CardinalRepresentative.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CardinalRepresentative.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.WellOrder.Base, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.CardinalRepresentative.md, https://bedrock.institute/ja/L.GCH.CardinalRepresentative.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Choosing a cardinal representative for an ordinal

Counting inside `L` is expressed in terms of cardinals, while a construction often produces an arbitrary ordinal. For an ordinal `α` of `L`, this chapter finds an internal cardinal `μ` contained in `α`, together with internal injections in both directions. Thus `μ` represents the cardinality of `α` inside the model. The representative is obtained by searching the successor of `α` for the least ordinal into which `α` internally injects.

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

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

module L.GCH.CardinalRepresentative {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

Fix excluded middle at level `ℓ-suc ℓ`. It is used by the well-order search and by ordinal trichotomy. All injections in the conclusion remain internal to `L`: their graphs are constructible sets rather than external functions.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Presentation {ℓ} using ( member; fiber )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL; isL-trans )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
```

Two structures are present. The ambient hierarchy supplies membership and the small presentations used for search. The constructible structure supplies the ordinal, cardinal and internal-injection predicates. Constructibility descends along membership, allowing a member found in the ambient hierarchy to be returned to the carrier of `L`.

```agda
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL; module LeastCardInjL )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( IsLeast; leastOf; module SWO )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

The search rests on the well-order of the indices presenting an ordinal. Its order agrees with membership between the represented elements. Inclusion coding turns containment into an internal injection, and transitivity composes successive internal injections.

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

The candidate set is the successor `sucV α`. Propositional truncation expresses the existence of a suitable representative without choosing one externally; sums and the empty type support the later trichotomy argument.

```agda
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( inl; inr )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

Write `SV.S` for ambient sets and `SL.S` for constructible sets. An element of `SL.S` pairs an ambient set with its constructibility certificate. Membership comparisons occur on first components, whereas `InjL` and `IsCardinalL` concern the complete constructible elements.

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropStructure 𝒮ᵥ using ( S )
module SL = hPropStructure 𝒮ʟ using ( S )
```

Given an ordinal `α`, the theorem merely asserts the existence of `μ` with five properties: `μ` is an ordinal, `μ` is an internal cardinal, `μ ⊆ α`, and there are internal injections `α ↪ μ` and `μ ↪ α`. The truncation makes the conclusion a proposition.

```agda
cardOf :
    (α : SL.S) → IsOrd (fst α)
  → ∥ Σ[ μ ∈ SL.S ]
       ( IsOrd (fst μ) × IsCardinalL μ
```

The final witness is assembled from the representative `μ` and the five proofs constructed below. Since the target is truncated, producing this single tuple closes the theorem once its components are available.

```agda
       × ((z : SV.S) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩)
       × InjL α μ × InjL μ α ) ∥₁
```

The auxiliary search setup for `α` supplies the successor's constructibility, the index naming `α` itself, the corresponding equality, and a well-order `w` on the presentation indices. The order relation of `w` is membership between the named ordinals.

```agda
cardOf α oα = ∣ μ , oμ , cardμ , μ⊆α , α↪μ , μ↪α ∣₁
  where
  module LC = LeastCardInjL α oα using ( hSucα; self; self-eq; w; w-lt )
```

Let `T` be the successor of the underlying ordinal `α`. The successor is again an ordinal, so every member of `T` is an ordinal and the order inherited from membership is available throughout the search.

```agda
  T : SV.S
  T = sucV (fst α)

  oT : IsOrd T
  oT = suc-ord oα
```

The set `T` is constructible. This certificate is needed because a search index names only an ambient member of `T`; downward closure of constructibility will turn that member into an element of `SL.S`.

```agda
  opaque
    hT : ⟨ isL T ⟩
    hT = LC.hSucα
```

For an index `b` of the presentation of `T`, `upL b` pairs the represented member with its constructibility proof. The latter follows from membership in `T` and the constructibility of `T`.

```agda
  upL : ⟪ T ⟫ → SL.S
  upL b = ⟪ T ⟫↪ b , isL-trans (member T b) hT
  Good : ⟪ T ⟫ → hProp (ℓ-suc ℓ)
  Good b = ∥ Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ b) × InjL α δ) ∥₁ , squash₁
```

Call an index `b` good when the member it names is the underlying set of some constructible `δ` and there is an internal injection `α ↪ δ`. The equality in `Good b` connects the indexed presentation with the constructible witness; truncation keeps goodness proposition-valued.

```agda
  selfGood : ⟨ Good LC.self ⟩
  selfGood = ∣ α , sym LC.self-eq , inclusion-coded α α (λ z z∈α → z∈α) ∣₁

  nonempty : ∥ Σ[ b ∈ ⟪ T ⟫ ] ⟨ Good b ⟩ ∥₁
  nonempty = ∣ LC.self , selfGood ∣₁
```

The index naming `α` is good: its represented member equals `α`, and the identity inclusion codes an internal injection from `α` to itself. Hence the type of good indices is merely inhabited.

```agda
  least : Σ[ b ∈ ⟪ T ⟫ ] IsLeast LC.w Good b
  least = leastOf LC.w lem Good nonempty

  m : ⟪ T ⟫
  m = fst least
```

Apply least-element search to the well-order `w` and the proposition-valued predicate `Good`. Excluded middle decides goodness, and nonemptiness guarantees a least good index. Denote that index by `m`.

```agda
  μ : SL.S
  μ = upL m

  μ∈T : ⟨ fst μ ∈ˢ T ⟩
  μ∈T = member T m
```

Lift the chosen index `m` to the constructible carrier and call the result `μ`. By construction its underlying set is the member of `T` named by `m`.

```agda
  oμ : IsOrd (fst μ)
  oμ = mem-ord {A = T} oT (fst μ) μ∈T
```

The presentation theorem gives `μ ∈ T`. Since `T` is an ordinal, every member of it is an ordinal; consequently `μ` is an ordinal as required.

```agda
  α↪μ : InjL α μ
  α↪μ = PT.rec squash₁ from (fst (snd least))
    where
    from : Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ m) × InjL α δ) → InjL α μ
```

Goodness of the least index supplies, under truncation, a constructible `δ`, an equality between its underlying set and the member named by `m`, and an injection `α ↪ δ`. The goal `InjL α μ` is a proposition, so the truncated witness may be eliminated into it.

```agda
    from (δ , e , α↪δ) =
      injl-trans α δ μ α↪δ
        (inclusion-coded δ μ (λ z z∈δ → subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈δ))
```

Transport along the indexed equality shows that `δ` is included in `μ`; inclusion coding turns this into an internal injection `δ ↪ μ`. Composing it with the supplied `α ↪ δ` proves `α ↪ μ`.

```agda
  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = snd (snd least) b bGood b<m
    where
    δ∈T : ⟨ fst δ ∈ˢ T ⟩
    δ∈T = oT .fst {x = fst μ} {y = fst δ} δ∈μ μ∈T
```

To prove that `μ` is a cardinal, suppose a member `δ ∈ μ` admitted an internal injection `μ ↪ δ`. Transitivity of the ordinal `T` places `δ` in `T`, so its presentation yields an index `b`.

```agda
    b : ⟪ T ⟫
    b = fiber T δ∈T .fst
    bδ : ⟪ T ⟫↪ b ≡ fst δ
```

The fibre theorem gives both the index `b` and the equality identifying its represented member with `δ`. These data let membership and injection statements be transported between the indexed member and the constructible element `δ`.

```agda
    bδ = fiber T δ∈T .snd
    bGood : ⟨ Good b ⟩
    bGood = ∣ δ , sym bδ , injl-trans α μ δ α↪μ μ↪δ ∣₁
```

The index `b` is good: compose `α ↪ μ` with the assumed `μ ↪ δ`, and use the fibre equality to match the indexed member. Thus `b` is another candidate in the same search.

```agda
    b<m : SWO._<∙_ LC.w b m
    b<m = transport (λ i → sym (LC.w-lt b m) i)
            (subst (λ z → ⟨ z ∈ˢ fst μ ⟩) (sym bδ) δ∈μ)
```

Moreover `b < m`. The relation of `w` is membership between represented ordinals, and the assumed `δ ∈ μ` transports to precisely this comparison. A good index strictly below the least good index is impossible, so no such injection `μ ↪ δ` exists. Hence `μ` is an internal cardinal.

```agda
  μ⊆α : (z : SV.S) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩
  μ⊆α = go (ord-tri (fst μ) oμ (fst α) oα)
    where
    go : Tri (fst μ) (fst α) → (z : SV.S) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩
```

It remains to show `μ ⊆ α`. Ordinal trichotomy compares their underlying ordinals. If `μ ∈ α`, transitivity of `α` gives the inclusion; if `μ = α`, transport gives it.

```agda
    go (inl μ∈α)       z z∈μ = oα .fst z∈μ μ∈α
    go (inr (inl e))   z z∈μ = subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈μ
```

The third case `α ∈ μ` contradicts minimality. The index naming `α` is good, and the membership `α ∈ μ` says that this index lies strictly below `m` in `w`. Thus only the first two trichotomy cases remain.

```agda
    go (inr (inr α∈μ)) z z∈μ =
      Empty.rec (snd (snd least) LC.self selfGood
        (transport (λ i → sym (LC.w-lt LC.self m) i)
          (subst (λ v → ⟨ v ∈ˢ fst μ ⟩) (sym LC.self-eq) α∈μ)))
```

The inclusion `μ ⊆ α` codes an internal injection `μ ↪ α`. Together with `α ↪ μ`, ordinalhood and cardinality of `μ`, it completes the promised representative. Any argument about the size of an ordinal may now pass to this internal cardinal without leaving `L`.

```agda
  μ↪α : InjL μ α
  μ↪α = inclusion-coded μ α μ⊆α
```

The representative `μ` is an ordinal cardinal internally injectable into `α` and receiving an internal injection from `α`, and it lies inside `α`. This reduces cardinal arithmetic on arbitrary constructible ordinals to cardinal arithmetic on internal cardinals.