可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

L 内部的计数以基数表述，而具体构造往往只产生任意序数。对 L 中的序数 α，本章找出包含于 α 的内部基数 μ，并给出两个方向的内部单射。因此，μ 在模型内部代表 α 的基数。构造在 α 的后继中搜索，选取 α 能够内部单射到的最小序数。

假设在层级 ℓ-suc ℓ 上成立排中律。良序搜索与序数三分法都会使用这个假设。结论中的单射全部位于 L 内部：它们由可构造的图见证，并非外部函数。

这里同时出现两个结构。外围层级提供成员关系以及搜索所用的小呈现；可构造结构提供序数、基数与内部单射谓词。可构造性沿成员关系向下传递，所以在外围层级中找到的元素可以重新进入 L 的论域。

搜索建立在呈现序数的索引良序之上；这个次序与所指元素之间的成员关系一致。包含关系的编码把包含化为内部单射，单射的传递性则复合连续的内部单射。

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

候选集合取为后继 sucV α。命题截断表达适当代表的存在，而不在外部选择一个代表；和类型与空类型用于后面的三分法论证。

以 SV.S 表示外围集合，以 SL.S 表示可构造集合。SL.S 的元素由外围集合及其可构造性证书组成。成员关系比较作用于第一分量，而 InjL 与 IsCardinalL 以完整的可构造元素为对象。

open hPropView 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropView 𝒮ᵥ using ( S )
module SL = hPropView 𝒮ʟ using ( S )

给定序数 α，定理仅仅断言存在满足五项性质的 μ：μ 是序数，是内部基数，满足 μ ⊆ α，并且存在内部单射 α ↪ μ 与 μ ↪ α。截断使整个结论成为命题。

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

最终见证由代表 μ 与下面构造的五项证明组成。由于目标已经截断，只要这些分量齐备，放入这个依值对即可完成定理。

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

关于 α 的辅助搜索准备提供后继的可构造性、指名 α 自身的索引及相应等式，还提供呈现索引上的良序 w。w 的次序关系就是所指序数之间的成员关系。

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

令 T 为序数 α 的底层集合的后继。后继仍是序数，因此 T 的每个元素都是序数，搜索全程都可使用由成员关系给出的次序。

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

  oT : IsOrd T
  oT = suc-ord oα

集合 T 是可构造的。这个证书不可或缺，因为搜索索引最初只指名 T 的外围元素；可构造性的向下封闭把该元素化为 SL.S 的元素。

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

对 T 的呈现索引 b，upL b 把所指元素与其可构造性证明配成依值对。后一个证明由该元素属于 T 以及 T 的可构造性得到。

  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 ∷ [])))

若存在从 α 到索引 b 所指可构造元素 upL b 的内部编码单射，就称 b 为好索引。包 definedGood 通过 injLAt 显露这个性质：两个环境槽分别放入 α 与 upL b，而 InjLAt.fill 和 InjLAt.read 证明语义的两个方向。因此，后续最小元搜索看到的是一条固定的对象语言公式，而不是任意宿主谓词。

  selfGood : ⟨ Good LC.self ⟩
  selfGood = inclusion-coded α α (λ z z∈α → z∈α)

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

指名 α 的索引是好的：它所指元素等于 α，恒等包含则编码出从 α 到自身的内部单射。因此，好索引的类型仅仅非空。

  least : Σ[ b ∶ ⟪ T ⟫ ] IsLeast LC.w Good b
  least = leastOfFormula LC.w definedGood lem nonempty

  m : ⟪ T ⟫
  m = least .fst

对良序 w 与 definedGood 应用面向公式的最小元搜索。排中律判定所展示单射公式的满足关系，非空性保证存在最小的好索引；把它记作 m。

  μ : SL.S
  μ = upL m

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

把选中的索引 m 提升到可构造论域，并把所得元素记作 μ。依定义，μ 的底层集合就是 m 在 T 中指名的元素。

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

呈现定理给出 μ ∈ T。由于 T 是序数，其每个元素仍是序数，所以 μ 具有所需的序数性。

  α↪μ : InjL α μ
  α↪μ = (least .snd) .fst

最小索引的合格性如今直接表述为由公式定义的命题 InjL α μ，因为 μ 正是 m 指名的可构造元素。因此，选中的候选立即给出正向单射。

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

为证明 μ 是基数，假设某个元素 δ ∈ μ 允许内部单射 μ ↪ δ。序数 T 的传递性给出 δ ∈ T，于是 T 的呈现产生一个指名 δ 的索引 b。

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

纤维定理同时给出索引 b 以及把它所指元素识别为 δ 的等式。这些数据使成员关系与单射陈述可以在索引元素和可构造元素 δ 之间搬运。

    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 α μ δ α↪μ μ↪δ)

索引 b 是好的：把 α ↪ μ 与假设的 μ ↪ δ 复合，再用纤维等式匹配索引所指的元素。于是 b 是同一次搜索中的另一个候选。

    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δ) δ∈μ)

而且 b < m。良序 w 的关系就是所指序数之间的成员关系，假设 δ ∈ μ 搬运后恰好给出这个比较。最小好索引之下不可能再有好索引，所以这样的单射 μ ↪ δ 不存在；因此 μ 是内部基数。

  μ⊆α : (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 ⟩

还需证明 μ ⊆ α。序数三分法比较二者的底层序数。若 μ ∈ α，由 α 的传递性得到包含；若 μ = α，沿等式搬运即可。

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

第三种情形 α ∈ μ 与最小性矛盾。指名 α 的索引是好的，而 α ∈ μ 表明这个索引在良序 w 中严格位于 m 之前。因此只剩三分法的前两种情形。

    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) α∈μ)))

包含 μ ⊆ α 编码出内部单射 μ ↪ α。连同 α ↪ μ 以及 μ 的序数性和基数性，这就完成了所承诺的代表。此后关于序数大小的论证可以在不离开 L 的前提下转到这个内部基数上。

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

代表 μ 是一个序数基数；它可以内部单射到 α，α 也可以内部单射到它，并且包含于 α。由此，任意可构造序数上的基数算术都可以化归为内部基数上的基数算术。

为序数选取基数代表