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

本论证以高于所讨论集合一个宇宙层级的排中律为参数。稍后会把同一假设降到较低层级，用来判定一个小命题，并将 Hartogs 关系编码为布尔值。这里不假设选择公理。

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

给定 L 中的一个无限基数，本章构造一个严格更大的基数，并由 L 中的序数表示。该构造只给出给定基数之上的一个显式候选；并不选取最小候选，那是后续装配工作的任务。

打开基础库，并在抬升层级取得排中律，再把它降到内层。后文有一条布尔值关系需要由它判定。

环境累积层级的两条性质推动后面的反证：成员关系是良基的，而且集合不属于自身。呈现为集合的元素提供索引，而 self∈sucV 把集合放入它的序数后继。

可构造一侧供给：其载体、传递的可构造性、序数谓词、可构造集合的层读取、序数事实，以及内部基数性谓词与其单射。

两座桥梁将连接整个构造。读取引理把 L 内部的编码单射变为呈现之间的实际单射，Mostowski 塌缩则把传递良基关系化为集合。借助二者，环境中的 Hartogs 论证最终给出内部基数陈述。

层级贡献成员关系桥、呈现、嵌入机制、带公理的分离构造，以及并运算。

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; ⋃_ )

证明只在公开陈述中使用 ω，并用序数后继建立上界。和类型表达序数三分法的各个分支，布尔值编码 Hartogs 构造所用的小关系；关于命题性的引理则保证稍后可以从截断存在中消去。

open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Bool using ( false≢true )

可达性与良基性，连同立方库的嵌入机制，支撑 Hartogs 一节的拉回论证。

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

空类型反驳不可能情形，而截断存在正是本章主结果的陈述形式。

外围结构与可构造结构都作为模块打开，因为两者贯穿全章。

module SV = hPropView 𝒮ᵥ
module SL = hPropView 𝒮ʟ

外围成员关系以朴素名字打开。

open SV using ( _∈ˢ_ )

环境基数性断言：对每个元素 δ ∈ κ，κ 的呈现都不能单射到 δ 的呈现。这里的单射是一个函数及其通常的单射性证明，并不是 Cubical 的嵌入记录。序数性是另一项性质，后文会为所构造的候选另行证明。

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

类型之间的单射通过复合映射并沿复合搬运单射性证明而复合。

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)

若 a ∈ b 且 b 是序数，则由传递性，a 的每个元素也是 b 的元素。因此，可把呈现 a 的一个元素的索引送到 b 的呈现在同一集合上的纤维，从而定义单射 ⟪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

该嵌入是单射的：两个索引的纤维同一视经由其像的等式串联。

  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)

目标陈述

公开目标给定可构造集合 κ，并假设其底层集合是序数、是内部基数且不属于 ω。结论只要求某个可构造集合 θ 的命题截断存在；不能从该定理中抽取特定见证。

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

产出的 θ 必须是序数、内部基数，且严格大于 κ；最后的成员关系表达的正是 von Neumann 序数的严格不等。

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

序数作为 L 的元素

外围序数通过「在其自身后继层处呈现」而成为 L 的元素：层 Lset (sucV x) 包含 x，其指数是序数，并携带 x 的可构造性。这是一个自然代表；本章不主张它是最早包含 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)

从环境基数性到内部基数性

环境基数性蕴涵内部基数性，且只有这一个方向。编码单射可由其读取引理读成环境单射，因此环境中的反驳消去截断的编码；由于目标是空类型，消去合法。

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

分出较小基数

固定集合 a 与序数界 β。这是 V ℓ 中的外围 Hartogs 构造，并非调用内部模型 L 的分离模式。它从 β 中分出呈现可单射到 a 的呈现的那些元素。所得集合先始终留在外围论证中，待独立证明其为序数后，才由「每个序数都可构造」这一事实放入 L。后续应用中的 a 也是序数，但在本模块内部只需要界的序数性。

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

分离谓词问：一个集合是否嵌入 a；它被陈述为截断的存在。由于它按构造居于 hProp ℓ，可直接交给分离，中间无需任何命题换级。

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

层级分离构造在该序数界处以这一谓词打开。

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

分离所得集合命名为 θ：它恰好收集界中那些可嵌入 a 的元素。

θ : SV.S
θ = SEPAREE

θ 中的成员关系由「属于界」连同「截断的到 a 嵌入」经分离公理引入。

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

反过来，θ 中的成员关系忘掉分离条件，只保留界中的成员关系。

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

分离条件只以「嵌入的截断存在」被恢复；并不从中选定任何具体嵌入。

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

分离所得集合 θ 是序数。下文先证明它自身的传递性；它的每个元素又因同时属于序数 β 而是传递集。这两点合起来正是 IsOrd θ。

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

为证传递性，取 y ∈ x ∈ θ。由于 x 是序数界的元素，它本身也是序数，所以成员关系给出从 y 到 x 的单射。把它与仅仅存在的 x 到 a 的单射复合，得到仅仅存在的 y 到 a 的单射；界的传递性还给出 y ∈ β，于是 θ-in 得到 y ∈ θ。

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

参数 a 一旦属于界，它就属于 θ：恒等映射见证它嵌入自身。

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

现在假设 θ ∈ β。若 θ 能单射到某个 δ ∈ θ，则 δ 的分离条件仅仅给出单射 δ ↪ a 的存在。两者在截断内复合，得到单射 θ ↪ a 的存在；再结合 θ ∈ β，分离规则便推出 θ ∈ θ，与反自反性矛盾。因此 θ 是环境基数。

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

还需证明 θ ∈ β，而界内只要有一个不能单射到 a 的序数 γ ∈ β 即已足够。三分法比较序数 θ 与 β；接下来的分支将排除相等情形以及 β 位于 θ 之下的情形。

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

三分法中只有 θ ∈ β 能够成立，此时结论直接得到。若 θ ≡ β，沿等式运输 γ ∈ β 会使 γ 成为 θ 的元素；其分离条件随即与「不存在单射 γ ↪ a」的假设矛盾。若 β ∈ θ，包含关系 θ ⊆ β 又会推出 β ∈ β。因此这里只把 θ 定位在所选上界之下，并未断言它是满足某种性质的最小序数。

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

归结为环境上界

Hartogs 输入以其最弱形式陈述：对每个序数，都存在某个序数不能单射入它。该类型不携带可构造性、编码或最小性；截断存在只命名一个序数及其不可注入性。

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

位置性引理比较两个序数并断言前者属于后者。三分法判定三种情形，其中两种矛盾。

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

先命名序数到其自身的恒等单射。若第二序数低于或等于第一序数，经搬运的单射将与不可注入假设矛盾。

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

只有三分法的第三种情形存留，即所宣告的成员关系。

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

设已显式给出一个不能单射到 a 的序数 γ。由该见证形成的分离集是显式可得的，并被证明是序数、环境基数且严格位于 a 之上。外围的存在陈述仍可带有命题截断；本引理只是把已拆出的见证映为已拆出的结果。

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

取序数后继 sucV γ 作为分离所用的界。见证 γ 属于它自己的后继；引理 above 给出 a ∈ γ，再由后继序数的传递性得到 a 也属于该界。

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

所需的两个旁条件现在都可得到。由 a ∈ γ ∈ sucV γ 推出 a ∈ sucV γ，所以恒等单射把 a 放入分离集。另一方面，见证满足 γ ∈ sucV γ 且不能单射到 a，因而迫使分离集本身位于界内，使基数性证明得以应用。

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

环境存在定理恢复截断：由对每个序数都供给见证的 Hartogs 输入，它为给定序数 a 产出其上方的环境基数的截断存在。

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

现在把环境中的存在定理转入 L。关于 κ 的三项数学假设中，这个构造使用其序数性来调用环境定理。内部基数性以及 κ 不属于 ω 是所陈述结果保留的较强假设，适合稍后对无限基数的应用，但本存在性证明的步骤并未使用它们。

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

环境基数在其自身后继层处呈现为 L 的元素，其基数性经单向比较转入内部谓词，而 κ 位于其下的成员关系原样通过。

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

Hartogs 序数

Hartogs 构造在任意环境集合 a 上组织成一个模块。它不要求 a 本身是序数，就能产生一个不能单射到 a 的序数；只有稍后把不可注入性转成严格比较 a ∈ γ 时，才需要 a 的序数性。

module Hartogs (a : SV.S) where

a 的呈现上的关系是一个二元布尔值函数。

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

布尔关系对其两个参数成立，当其取值为布尔真；由于布尔值构成集合，这一读取是命题。

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

a 的呈现上的良基关系是一个传递且良基的布尔关系。它不要求线性或三歧性，因此该类型的元素还不是良序。

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

每条良基布尔关系都配有自己的塌缩模块。

module Col (w : WFR) where

固定这样一条关系 w。它的第一分量是布尔关系 R，其余分量分别证明传递性与良基性。塌缩论证将这些作用分开：关系决定成员关系，而证明保证递归有效并给出序数的传递性。

R : Rel
R = w .fst

在塌缩一侧，该关系以布尔成立的提升形式读取，从而居于 Mostowski 一章所期望的层级。

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

提升后的关系继承原 Bool 值关系的传递性。先降低两条提升后的假设，便得到可由 w 中所存传递性复合的布尔等式；再提升结果，即回到塌缩所要求的宇宙层级。

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

同样的宇宙层级变换也保持良基性。go 从 Bool 值关系的可及性树出发，递归地把每条前驱边换成其提升版本，从而得到 _≺_ 的可及性树。

≺-wf : WellFounded _≺_
≺-wf x = go x ((w .snd) .snd 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)))

提升后的关系现已满足 Mostowski 构造的两项假设：它既传递又良基。因此可以使用其塌缩 col；配套定律刻画各塌缩值中的成员关系，并证明每个塌缩值都是序数。

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

把所有塌缩值收集为其像 ot。名称虽暗示序型，但 WFR 的任意元素未必是良序，此处也没有断言唯一性或同构定理。论证所需的只是证明这个像为序数。

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

每个 col p 都属于该像。这里给出的见证是索引 p 与自反等式，并包在命题截断中，因为像中的成员关系只保留某个原像存在这一事实。

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

这个像是序数。首先，像的元素仅仅等于某个塌缩值，而该塌缩值是序数，所以该元素传递。其次，像自身传递：若 y ∈ x 且 x 由 col p 表示，col-out 仅仅把 y 表示成某个前驱 r 的 col r；随后 r 的典范像见证便给出 y ∈ ot。两次截断存在都只消去到命题值的成员关系或传递性目标中。

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

元素的传递性沿呈现等式从塌缩的序数性运输而来，而外层消去消耗该元素在像内截断的分解。

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

截断的分解给出索引 r，使其坍缩为 y，并证明 r 先于 p。坍缩定律把 col r 放入 col p，而典范像见证 ot-in r 把 col r 放入 ot。沿等式 col r ≡ y 运输，便得到 y ∈ ot。

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

Hartogs 候选 μ 是 WFR 所产生全部塌缩像的后继之并。纳入每个像的后继，而非仅纳入像本身，保证每个 Col.ot w 都严格属于这一公共上界。该构造界住所有这些像，却不声称其中任何一个是唯一确定的序型。

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

上界序数是序数，由界引理从族中每个元素皆为序数这一事实证明。

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

对每个 w : WFR，其塌缩像 Col.ot w 都属于 μ。这个严格上界预先提供最终矛盾的一半：一旦对从假设单射拉回的关系得到反向包含 μ ⊆ Col.ot w，便会推出自成员关系。

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

对环境累积层级中的任意集合 x，其呈现类型 ⟪ x ⟫ 都嵌入层级本身。层级是 h-集合，因此呈现类型也是 h-集合。于是，到 ⟪ a ⟫ 的普通单射性可以提升为纤维具有命题性。

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

判定器把经典情形分裂转为布尔值，将两支编码为 true 与 false。

decB : {A : Type ℓ} → Dec A → Bool
decB (yes _) = true
decB (no _)  = false

排中律实例从后继层级降到工作层级，使工作层级上的命题可被判定。

lemℓ : LEM ℓ
lemℓ = lowerLEM lem

为导出矛盾，假设有单射 f : ⟪ μ ⟫ ↪ ⟪ a ⟫。接下来的构造把 μ 的呈现元素之间的成员关系运到该单射的像上，从而得到一个已包含在 WFR 族中的关系。

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

嵌入的底层函数为后续构造只命名一次。

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

由于源与目标都是 h-集合，单射函数是嵌入：每个纤维是命题。

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

一点上的纤维由 μ 的元素索引以及一条等式组成，该等式说明 F 把这个索引映到该点。因此，Fib x 的元素恰好是 x 位于 F 的像中的一种呈现。

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

F 的每个纤维都是命题。因此，两条拉回关系证明即使以可能不同的索引表示同一个像点，这两个纤维元素也必然相等。这种唯一性用于对齐代表；它不会为像外的点选择代表。

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

关系 PreT x y 首先要求实际的纤维见证，说明 x 与 y 都在 F 的像中；随后规定，当且仅当相应的 μ 呈现元素满足小成员关系时，x 先于 y。因此，像外的点在该关系中没有前驱。

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

拉回前驱关系是命题：由两个命题纤维与一个成员关系命题构成。

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

布尔关系是拉回前驱关系的可判定编码，由对命题值关系应用排中律而得。

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

若布尔关系成立，其值便等于 true。检查排中律给出的判定即可恢复 PreT x y：肯定支含有所需证明；否定支会迫使布尔值为 false，因而导致矛盾。

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 : Dec (PreT x y)) → decB d ≡ true → PreT x y
  go (yes h) _ = h

反驳支不可能：若前驱事实不成立，判定器将返回 false，与 true 成员关系矛盾。

  go (no _) e' = ⊥₀-rec (false≢true e')

向后读法由同一经典判定，从拉回前驱事实构造布尔成员关系。

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 : Dec (PreT x y)) → decB d ≡ true
  go (yes _) = refl

空支不可能：前驱事实由假设成立。

  go (no n) = ⊥₀-rec (n h)

为证明传递性，先把 x R y 与 y R z 解读为两条 PreT 见证。它们共含四条纤维见证：x 上一条、共同中点 y 上两条、z 上一条。由于 y 上的纤维是命题，其中两条见证相等，因而可以对齐它们所表示的 μ 元素。随后利用最后一个表示元素的传递性复合两步成员关系，得到 x R z 的 PreT 见证。

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

解读第一条关系得到 x 与 y 上的索引 p、q；解读第二条关系得到 y 与 z 上的索引 q'、r。y 上纤维的命题性把 q 与 q' 认同，因而可将第一条关系所表示的成员关系改写为使用与第二条关系相同的中间索引。

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

最终元素 r 被命名，其传递性由 μ 的序数性读取。

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

两条成员关系经 r 的传递性复合产出目标：第一元素在第三元素之内，这正是拉回关系所需的。

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

良基性由环境层级中正则公理所给的良基性沿嵌入搬运。辅助引理处理目标已知等于特定层级元素的情形。

辅助证明为给定元素的每个前驱构造可达性。

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

元素的每个前驱 r 被分解为由拉回关系连接的两个 μ 元素，可达性被运到第一分量。

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

前驱事实给出 p 与 q：p 是 r 在 μ 中的代表，q 是 F m 在 μ 中的代表。

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

F m 上的两条纤维见证相等，因为该纤维是命题。沿这一等式运输，可把解读出的关系改写为：p 所表示的前驱属于 m 所表示的元素。再利用后一个元素与 v 的等式，便把前驱严格置于 v 之下，从而可以应用可达性递归。

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

拉回关系的良基性来自环境层级的正则公理：任何元素的每个前驱都严格低于某个层级元素，辅助引理在该处产出可达性。

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)) (p .snd)

对 x 的任意前驱 r，解读该关系会给出 r 上的纤维见证 p。正则公理给出其索引所表示的层级元素的可达性，wfAux 再把这份可达性传回点 F (p .fst)。纤维等式把该点与 r 认同，从而完成所需的可达性证明。

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

良基传递关系连同其两条证明被打包，完成上界序数所遍历的良基关系族。

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

把塌缩构造应用于由假设单射得到的特定关系 w。下文将直接比较其塌缩值及其像与 μ 的呈现元素；论证不需要声称 w 是良序。

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

关键引理说：拉回关系的塌缩重现了上界序数的元素。对呈现为层级元素的每个 μ 元素，其像的塌缩等于该元素。证明是对层级元素的良基归纳。

证明在两个方向上以外延性比较元素。

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

先证向前包含。设 b 属于 col (F m)。消去定律 col-out 仅仅断言：b 是 F m 的某个前驱 r 的塌缩值。经 PreT 解码此前驱，可得到一个位于 m 之下的索引；归纳假设将把该索引所表示的元素与 col r，继而与 b 认同。

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

前驱见证由 r ≺ F m 与等式 col r ≡ b 组成。经 R→Pre 读回关系证明，可得到 r 与 F m 的纤维；其中的索引标识相应的 μ 呈现元素，最后一个分量则记录二者之间的成员关系。

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

F m 上的纤维具有命题性，所以由关系证明得到的代表 q 等于显然的代表 (m , refl)。沿此等式运输，解码后的成员关系便成为「前驱索引属于 m 所表示的集合」这一陈述。

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

利用等式 ⟪ μ ⟫↪ m ≡ v，上述成员关系把前驱所表示的集合置于环境成员关系中的 v 之下。因此可以在此前驱处使用递归假设，把其塌缩值与其所表示的集合认同。

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

归纳假设把解码索引的塌缩值与该索引所表示的元素认同。纤维等式又把该索引的像与 r 认同，因此对 col 使用同余便得到呈现元素与 col r 之间所需的等式；再与 col r ≡ b 复合，即完成向前包含。

      cpr = sym ih ∙ cong col (p .snd)

再证反向包含。现从 b 属于索引 m 所表示的集合出发，目标是证明 b ∈ col (F m)。序数 μ 的传递性先把 b 提升为 μ 的元素，于是 μ 的典范呈现可以给出表示 b 的索引 k。

  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 ⟩

这里 fiber μ b∈μ 返回实际索引 k 与等式 ⟪ μ ⟫↪ k ≡ b。这是因为小成员关系 _∈ₛ_ 基于典范呈现中具有命题性的纤维。它是该呈现的局部逆过程，并非从任意截断存在中作选择。

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

fiber 返回的等式把原有成员关系 b ∈ ⟪ μ ⟫↪ m 改写为呈现元素 ⟪ μ ⟫↪ k 的成员关系。随后，显然的两个纤维 (k , refl)、(m , refl) 与这条成员关系共同建立 PreT (F k) (F m)。

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

把这条 PreT 事实编码为 Bool 关系，可得 F k ≺ F m。因此，塌缩引入定律把 col (F k) 放入 col (F m)。与此同时，呈现元素属于 m 所表示集合这一事实把它置于归纳参数 v 之下，所以递归假设可用于 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

递归假设给出 col (F k) ≡ ⟪ μ ⟫↪ k。把它与纤维等式 ⟪ μ ⟫↪ k ≡ b 复合，便可把刚构造的成员关系运输为 b ∈ col (F m)，从而完成反向包含。

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

正则公理为 μ 的每个索引 m 提供专门化该归纳所需的可及性证明。因此，key' 把 col (F m) 与 m 所表示的元素认同。证明的下一部分才会用这些逐点等式建立包含 μ ⊆ Col.ot w；此处尚未断言该包含。

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

μ 的每个元素 b 也属于坍缩像 ot。μ 在 b 处的典范纤维给出索引 m，满足 ⟪ μ ⟫↪ m ≡ b。引理 key' 把这个代表与 col (F m) 识别，而 ot-in 把该坍缩值放入 ot；沿这两个等式传输，便得到 b ∈ ot。

因此，这段论证只建立包含关系 μ ⊆ ot。结合 ot ∈ μ，这一包含关系已经足以导出矛盾，无须证明 μ 与 ot 相等或序同构。

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

典范呈现的纤维具有命题性，因此为 b 恢复出的代表唯一确定。把这个代表及其等式合记为 fb，便同时为前述包含证明中的 key' 与 ot-in 提供所需索引。

  fb = fiber μ b∈μ

由上界的构造，ot 是 μ 的元素。把包含关系 μ ⊆ ot 用于这个特定元素，便得到 ot ∈ ot，与成员关系的非自反性矛盾。这样，由假设的单射 μ ↪ a 所引出的矛盾便告完成。

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

上述局部矛盾是在任意单射 f : ⟪ μ ⟫ ↪ ⟪ a ⟫ 的假设下证明的。定理 noInj 现在把这一结论带到 Hartogs 模块的接口上：每一条候选单射都会给出上面的拉回关系，因而导出 ⊥*。

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

所得的更大 L 基数

对每个序数 x，显式对象 Hartogs.μ x 是序数，并且不能单射入 x。随后把这个对象及其序数性和不可注入性置于命题截断之下，便得到 NoInjOrd。因此，打包之前已有确定的见证，而调用者只取得它的截断存在性。

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

最后，noInjOrd→CardAboveLᵀ 把 Hartogs 见证变成一个严格更大的环境序数基数，把该序数放入 L，再将其环境基数性传递为内部基数性。所得存在性经过命题截断：对给定的序数基数 κ，存在某个可构造的内部基数 θ，满足 κ ∈ θ。

这个定理为后续的后继基数构造保证所需候选非空，但并不选出其中的最小者。L.GCH.Assembly 先用这里的见证限定搜索范围，再完成最小化。

CardAboveL : CardAboveLᵀ
CardAboveL = noInjOrd→CardAboveLᵀ noInjOrd

任意 L 基数之上的序数 L 基数