---
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, FOL.Semantics, V.Hierarchy, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.WellOrder.Base, L.DefinableInjection, 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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# Choosing a cardinal representative for an ordinal

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

Fix a universe level `ℓ` and assume `lem : LEM (ℓ-suc ℓ)`. This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

```agda
open import FOL.ZFStructure using ( module hPropView )
import FOL.Semantics
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 )
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; leastOfFormula; module SWO )
open import L.DefinableInjection {ℓ} lem using ( injLAt; module InjLAt )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

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.

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.

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`.

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.

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 hPropView 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropView 𝒮ᵥ using ( S )
module SL = hPropView 𝒮ʟ 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 = InjL α (upL b) , squash₁

  definedGood : FOL.Semantics.FormulaPredicate 𝒮ʟ ⟪ T ⟫ SL.S id Good
  definedGood = FOL.Semantics.presented 2 (injLAt zero (suc zero))
    (λ b → α ∷ upL b ∷ [])
    (λ b → ⇔toPath
      (InjLAt.fill zero (suc zero) (α ∷ upL b ∷ []))
      (InjLAt.read zero (suc zero) (α ∷ upL b ∷ [])))
```

Call an index `b` good when there is an internal coded injection from `α` to the constructible member `upL b` that it names. The package `definedGood` exposes this property through `injLAt`: its two environment slots contain `α` and `upL b`, while `InjLAt.fill` and `InjLAt.read` prove the two semantic directions. Thus the later least search sees a fixed object-language formula rather than an arbitrary host predicate.

```agda
  selfGood : ⟨ Good LC.self ⟩
  selfGood = 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 = leastOfFormula LC.w definedGood lem nonempty

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

Apply the formula-facing least-element search to the well-order `w` and `definedGood`. Excluded middle decides satisfaction of the displayed injection formula, 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 α μ
  α↪μ = (least .snd) .fst
```

Goodness of the least index is now stated directly as the formula-defined proposition `InjL α μ`, because `μ` is the constructible member named by `m`. Thus the selected candidate immediately supplies the forward injection.

```agda
  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = (least .snd) .snd 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
    bS : upL b ≡ δ
    bS = Σ≡Prop (λ x → (isL x) .snd) bδ
    bGood : ⟨ Good b ⟩
    bGood = subst (InjL α) (sym bS) (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 : let module W = SWO LC.w in b W.<∙ 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∈μ =
      ⊥₀-rec ((least .snd) .snd 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.