---
title: "任意の L 基数より大きい順序数 L 基数"
module: L.CardinalAbove
lang: ja
site: "Bedrock"
description: "任意の L 基数より大きい順序数 L 基数"
stage: "順序数，単射，基数"
reading_order: 96
canonical: https://bedrock.institute/ja/L.CardinalAbove.html
html: L.CardinalAbove.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/CardinalAbove.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Presentation, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Cardinal, L.CantorBernstein, L.Mostowski]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.CardinalAbove.md, https://bedrock.institute/zh/L.CardinalAbove.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 任意の L 基数より大きい順序数 L 基数

`L` の無限基数が与えられたとき、この章は真に大きい基数を構成し、それを `L` の順序数で表します。構成は、与えられた基数より上の一つの明示的な候補を作るだけで、最小の候補を選ぶのは後の組み立ての仕事です。

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

基礎ライブラリを開き、上げられたレベルで排中律を受け取り、さらに内側のレベルへ降ろします。後で、ブール値の関係をこれで判定するためです。

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

この議論は、対象となる集合より一つ高い宇宙レベルの排中律を引数に取ります。後で同じ仮定を低いレベルへ移し、小さな命題を判定して Hartogs の関係をブール値で符号化します。選択公理は仮定しません。

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

周囲の累積階層における二つの性質が、後の背理法を支えます。所属は整礎的であり、どの集合も自分自身には属しません。提示は集合の要素に添字を与え、`self∈sucV` は集合をその順序数としての後続に入れます。

```agda
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 {ℓ}
```

構成可能な側は、その台、推移的な構成可能性、順序数の述語、構成可能な集合の段階の読み、順序数の事実、そして内部の基数性の述語とその単射を供給します。

```agda
  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; _↪_ )
```

二つの橋渡しが構成を結びます。読み取り補題は `L` 内部の符号化された単射を提示の間の実際の単射に変え、Mostowski 崩壊は推移的で整礎的な関係を集合へ移します。これらにより、周囲での Hartogs の議論から内部の基数に関する主張が得られます。

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

階層は、所属の橋、提示、埋め込みの仕組み、公理を伴う分出の構成、そして和の演算を供給します。

```agda
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 の構成で用いる小さな関係を符号化します。命題性に関する補題は、後で切り詰められた存在から除去できることを保証します。

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

到達可能性と整礎性、そして Cubical ライブラリの埋め込みの仕組みが、Hartogs の節の引き戻しの議論を支えます。

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

空の型は不可能な場合を反証し、切り詰められた存在が、この章の主な結果の述べ方です。

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

周囲の構造と構成可能な構造の両方が、全章を通して使われるため、モジュールとして開かれます。

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

周囲の所属が、そのままの名前で開かれます。

```agda
open SV using ( _∈ˢ_ )
```

周囲での基数性は、各要素 `δ ∈ κ` に対して、`κ` の提示から `δ` の提示への単射が存在しないことを述べます。ここでいう単射は、通常の単射性の証明を伴う関数であり、Cubical の埋め込みレコードではありません。順序数性は別の性質であり、後で構成する候補について独立に証明します。

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

型の間の単射は、写像を合成し、単射性の証明を合成を通して運ぶことで合成されます。

```agda
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⟫` を定めます。

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

埋め込みは単射です。二つの索引の繊維の同一視が、像の等式を通して連鎖するからです。

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

## 目標となる主張

公開された目標は、構成可能な `κ` と、その台となる集合が順序数であり、内部の基数であり、`ω` の要素ではないという証明を受け取ります。結論が要求するのは構成可能な `θ` の命題的に切り詰められた存在だけであり、定理から特定の証人を取り出すことはできません。

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

産み出される `θ` は順序数であり、内部の基数であり、`κ` より真に大きくなければなりません。最後の所属が、von Neumann 順序数としての狭義の不等号を表します。

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

## L の要素としての順序数

周囲の順序数は、その自身の後続の段階で提示されることで、`L` の要素になります。段階 `Lset (sucV x)` は `x` を含み、その指数は順序数であり、`x` の構成可能性を運びます。これは自然な代表であり、`x` を含む最も早い段階だと主張するものではありません。

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

## 周囲の基数性から内部の基数性へ

周囲の基数性は内部の基数性を含意します。ただし一方向だけです。符号化された単射はその読みの補題によって周囲の単射として読めるので、周囲での反証が切り詰められた符号を消去します。目標が空の型であるため、この消去は正当です。

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

## より小さい基数を分出する

集合 `a` と順序数の上界 `β` を固定します。この構成は、提示から `a` の提示への単射をもつ要素を `β` から分出します。後の適用では `a` も順序数ですが、このモジュールの内部で必要なのは上界の順序数性だけです。

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

分出の述語は、ある集合が `a` へ埋め込めるかを問い、切り詰められた存在として述べられます。それは構成によって `hProp ℓ` に住むので、中間の命題リサイズなしに、そのまま分出に渡せます。

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

階層の分出の構成が、この述語とともに、順序数の上界のもとで開かれます。

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

分出された集合は `θ` と名付けられます。それは、上界の要素のうち `a` へ埋め込めるものをちょうど集めた集合です。

```agda
  θ : SV.S
  θ = SEPAREE
```

`θ` の中の所属は、上界への所属と、`a` への切り詰められた埋め込みとを、分出の公理を通して導入されます。

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

逆に、`θ` の中の所属は分出の条件を忘れ、上界への所属だけを残します。

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

分出の条件は、埋め込みの切り詰められた存在としてのみ復元されます。具体的な埋め込みが選ばれることはありません。

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

分出された集合 `θ` は順序数です。`θ` 自身の推移性は以下で示します。また、その各要素は順序数 `β` の要素でもあるため推移的です。この二つを合わせると `IsOrd θ` が得られます。

```agda
  θ-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 ∈ θ` となります。

```agda
      θ-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∈θ))
```

引数 `a` は、上界に属すれば `θ` にも属します。恒等写像が、自分自身への埋め込みを証明するからです。

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

ここで `θ ∈ β` と仮定します。`θ` からある `δ ∈ θ` への単射があれば、`δ` の分出条件から、単射 `δ ↪ a` が単に存在することが得られます。切り詰めの中で両者を合成すると、単射 `θ ↪ a` が単に存在します。これと `θ ∈ β` を分出の規則に入れると `θ ∈ θ` となり、非反射性に矛盾します。したがって `θ` は周囲の基数です。

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

残る課題は `θ ∈ β` の証明であり、`a` へ単射できない順序数 `γ ∈ β` が一つあれば十分です。三分性によって二つの順序数 `θ` と `β` を比較し、次の各場合で等しい場合と `β` が `θ` より下にある場合を退けます。

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

三分性のうち成立しうるのは `θ ∈ β` だけで、この場合は結論が直ちに得られます。`θ ≡ β` なら、`γ ∈ β` を等式に沿って運ぶことで `γ ∈ θ` となり、その分出条件が単射 `γ ↪ a` は存在しないという仮定に反します。`β ∈ θ` なら、包含 `θ ⊆ β` から `β ∈ β` が従い、やはり矛盾します。ここで示したのは `θ` が選んだ上界より下にあることだけで、何らかの性質をもつ最小の順序数だとは述べていません。

```agda
    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 β (θ⊆β β β∈θ))
```

## 周囲の上界へ帰着する

Hartogs の入力は、最も弱い形で述べられます。すべての順序数に対して、それに単射しない順序数が存在する、ということです。この型は構成可能性も符号化も最小性も運びません。切り詰められた存在が名指すのは、順序数とその非単射性だけです。

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

位置づけの補題は、二つの順序数を比較し、最初のものが二つ目に属することを結論します。三岐性が三つの場合を判定し、そのうち二つは矛盾します。

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

まず、順序数から自分自身への恒等単射に名前を付けます。二つ目の順序数が一つ目より下か等しいなら、運ばれた単射が非単射性の仮定と矛盾します。

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

三岐性の三つ目の場合だけが残り、それが宣言された所属です。

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

`a` へ単射できない順序数 `γ` が明示的に与えられたとします。この証人から作る分出集合は明示的に得られ、順序数であり、周囲の基数であり、`a` より真に大きいことが証明されます。外側の存在の主張は切り詰められていてもよく、この補題は取り出された証人を取り出された結果へ写します。

```agda
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γ
```

分出の上界として順序数の後続 `sucV γ` を使います。証人 `γ` は自分自身の後続に属します。補題 `above` から `a ∈ γ` が得られ、後続順序数の推移性により `a` もこの上界に属します。

```agda
  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` へ単射できないため、分出集合自身が上界の中にあることが強制され、基数性の証明を適用できます。

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

周囲の存在定理が切り詰めを回復します。すべての順序数に証人を供給する Hartogs の入力から、与えられた順序数 `a` の上の周囲の基数の、切り詰められた存在を産み出します。

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

ここで、周囲での存在定理を `L` へ移します。`κ` に関する三つの数学的仮定のうち、この構成が周囲の定理を適用するために使うのは順序数性です。内部での基数性と `ω` に属さないことは、後で無限基数に適用するのに適した、定理のより強い仮定ですが、この存在証明の各段階では使われません。

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

周囲の基数は、その自身の後続の段階で `L` の要素として提示され、その基数性は一方向の比較によって内部の述語へ運ばれ、`κ` がその下に属することはそのまま通ります。

```agda
        → Σ[ θ ∈ 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 ∈ γ` へ変えるときだけです。

```agda
module Hartogs (a : SV.S) where
```

`a` の提示の上の関係は、二つの引数をもつブール値の関数です。

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

ブールの関係が二つの引数について成立するのは、その値がブールの真であるときです。ブール値は集合を作るので、この読みは命題です。

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

`a` の提示の上の整礎的な関係とは、推移的かつ整礎的なブールの関係です。線形性や三岐性は要求されないので、この型の要素はまだ整列順序ではありません。

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

整礎的なブールの関係のそれぞれに、固有の崩壊のモジュールが用意されます。

```agda
  module Col (w : WFR) where
```

このような関係 `w` を一つ固定します。第一成分はブール関係 `R` であり、残りの成分が推移性と整礎性を保証します。崩壊の議論ではこれらの役割を分けます。関係が所属を定め、証明が再帰の正当性と順序数の推移性を与えるからです。

```agda
    R : Rel
    R = fst w
```

崩壊の側では、関係は、ブールが成立することを持ち上げた形で読まれます。これで、Mostowski の展開が期待するレベルに合うのです。

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

持ち上げた関係は、もとの Bool 値関係から推移性を受け継ぎます。二つの仮定をいったん下ろすと、`w` に収められた推移性で合成できるブール等式が得られ、その結果を再び持ち上げれば、崩壊が要求する宇宙レベルに戻ります。

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

同じ宇宙レベルの変更によって整礎性も保たれます。`go` は Bool 値関係の到達可能性の木から出発し、各前者の辺を持ち上げた辺に再帰的に置き換えて、`_≺_` の到達可能性の木を作ります。

```agda
    ≺-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)))
```

持ち上げた関係は、Mostowski の構成に必要な二つの仮定、すなわち推移性と整礎性を満たしました。そこで、その崩壊 `col` を使えます。付随する法則は各崩壊値の所属を記述し、すべての崩壊値が順序数であることを示します。

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

すべての崩壊値を像 `ot` として集めます。この名前は順序型を思わせますが、`WFR` の任意の要素が整列順序であるとは限らず、ここでは一意性や同型に関する定理も主張しません。必要なのは、この像が順序数であることだけです。

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

各 `col p` はこの像に属します。ここで与える証人は添字 `p` と反射律であり、像への所属は逆像が存在することだけを残すため、命題的切り詰めで包まれています。

```agda
    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` が得られます。二つの切り詰められた存在はいずれも、命題値の所属または推移性の目標にだけ除去されます。

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

要素の推移性は、崩壊の順序数性から、提示の等式に沿って運ばれ、外側の消去が、像の中のその要素の切り詰められた分解を消費します。

```agda
        (λ 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 ⟩
```

切り詰められた分解から、崩壊が `y` であり、かつ `p` に先行する添字 `r` が得られます。崩壊の法則は `col r` を `col p` に入れ、正準な像の証人 `ot-in r` は `col r` を `ot` に入れます。したがって、等式 `col r ≡ y` に沿って運べば `y ∈ ot` が得られます。

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

Hartogs の候補 `μ` は、`WFR` から得られるすべての崩壊像の後続の和集合です。像そのものだけでなく各像の後続を入れることで、すべての `Col.ot w` がこの共通上界に真に属することが保証されます。この構成はそれらの像を一括して抑えますが、どの像についても一意に定まる順序型だとは主張しません。

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

上界の順序数は順序数です。族のすべての要素が順序数であるという事実から、上界の補題によって証明されます。

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

各 `w : WFR` について、その崩壊像 `Col.ot w` は `μ` に属します。この厳密な上界は、最後の矛盾の半分をあらかじめ与えます。仮定した単射から引き戻した関係について逆向きの包含 `μ ⊆ Col.ot w` が得られれば、自己所属が従います。

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

周囲の累積階層の任意の集合 `x` について、その提示型 `⟪ x ⟫` は階層そのものへ埋め込まれます。階層は h-集合なので、提示型も h-集合です。これにより、`⟪ a ⟫` への通常の単射性を、ファイバーが命題であるという性質へ引き上げられます。

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

判定器は、古典的な場合分けをブール値に変え、二つの分岐を `true` と `false` に符号化します。

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

排中律の実例は、後続のレベルから作業のレベルへ降ろされ、作業のレベルに住む命題を判定できるようにします。

```agda
  lemℓ : LEM ℓ
  lemℓ = lowerLEM lem
```

矛盾を導くため、単射 `f : ⟪ μ ⟫ ↪ ⟪ a ⟫` があると仮定します。以下では、`μ` の提示された要素間の所属をこの単射の像へ移し、すでに族 `WFR` に含まれる関係を作ります。

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

埋め込みの基礎となる関数が、以降の構成のために一度だけ名づけられます。

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

源も目標も h-集合なので、単射な関数は埋め込みです。それぞれのファイバーは命題です。

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

ある点上のファイバーは、`μ` の要素の添字と、`F` がその添字をその点へ写すことを示す等式からなります。したがって、`Fib x` の要素は、`x` が `F` の像に属することの提示にほかなりません。

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

`F` の各ファイバーは命題です。したがって、二つの引き戻し関係の証明が同じ像の点を異なるかもしれない添字で提示しても、それらのファイバー要素は等しくなります。この一意性は代表を揃えるために使われ、像の外の点に代表を選ぶものではありません。

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

関係 `PreT x y` はまず、`x` と `y` がともに `F` の像にあることを示す実際のファイバーを要求します。そのうえで、対応する `μ` の提示要素が小所属関係にあるとき、ちょうどそのときに `x` が `y` に先行すると定めます。したがって、像の外の点にはこの関係での前者がありません。

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

引き戻された前者の関係は命題です。二つの命題であるファイバーと一つの所属の命題からできています。

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

ブールの関係は、引き戻された前者の関係の、判定可能な符号化です。命題値の関係に排中律を適用することで得られます。

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

ブール関係が成り立つなら、その値は `true` です。排中律による判定を調べると `PreT x y` を復元できます。肯定側には求める証明があり、否定側ではブール値が `false` になるため矛盾します。

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

反駁の分岐は不可能です。前の事実が成立しなければ、判定器は `false` を返し、`true` の所属と矛盾します。

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

後ろ向きの読み出しは、同じ古典的な判定によって、引き戻された前者の事実からブールの所属を作ります。

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

空の分岐は不可能です。前の事実は仮定によって成立するからです。

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

推移性を示すため、`x R y` と `y R z` を二つの `PreT` の証人として読み取ります。そこには四つのファイバーの証人があります。`x` 上に一つ、共通の中間点 `y` 上に二つ、`z` 上に一つです。`y` 上のファイバーは命題なので二つの証人は等しく、対応する `μ` の要素を揃えられます。そこで最後の提示要素の推移性を使って二段階の所属を合成すると、`x R z` に対する `PreT` の証人が得られます。

```agda
    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'` が同一視され、第一の関係が表す所属を、第二の関係と同じ中間の添字を使う形に書き換えられます。

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

最後の要素 `r` が名づけられ、その推移性は `μ` の順序数性から読まれます。

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

二つの所属の関係を、`r` の推移性を通して合成すると、目標が作られます。第一の要素が第三の要素の中にあること、これが引き戻された関係の要求です。

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

整礎性は、周囲の階層の正則性から、埋め込みに沿って運ばれます。補助の補題は、目標が特定の階層の要素と等しい場合を扱います。

補助の証明は、与えられた要素のそれぞれの前者に対して、アクセス可能性を構成します。

```agda
    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` は、引き戻された関係で結ばれた二つの `μ` の要素に分解され、アクセス可能性は第一の成分へ運ばれます。

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

前の事実から、`p` と `q` が得られます。`p` は `r` の `μ` の中の代表であり、`q` は `F m` の `μ` の中の代表です。

```agda
        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) ⟩)
```

`F m` 上の二つのファイバーの証人は、そのファイバーが命題なので等しくなります。この等式に沿って運ぶと、読み取った関係は、`p` が表す先行要素が `m` の表す要素に属するという形に書き換えられます。後者を `v` と同定する等式によって先行要素は `v` より真に下に置かれ、そこで到達可能性の再帰を適用できます。

```agda
              (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)
```

引き戻された関係の整礎性は、周囲の階層の正則性から従います。ある要素のそれぞれの前者は、ある階層の要素より厳密に下にあり、補助の補題がそこでアクセス可能性を作ります。

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

`x` の任意の先行要素 `r` に対して、関係を読み取ると `r` 上のファイバーの証人 `p` が得られます。正則性は、その添字が表す階層の要素の到達可能性を与え、`wfAux` がその到達可能性を点 `F (fst p)` へ移します。ファイバーの等式がこの点を `r` と同定し、必要な到達可能性の証明が完成します。

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

整礎で推移的な関係が、その二つの証明とともにまとめられ、上界の順序数がわたる整礎な関係の族が完成します。

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

仮定した単射から得た特定の関係 `w` に崩壊の構成を適用します。以下では、その崩壊値と像を `μ` の提示要素と直接比較します。`w` が整列順序であるという主張は必要ありません。

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

重要な補題はこう言います。引き戻された関係の崩壊は、上界の順序数の要素を再現します。階層の要素として提示された `μ` の各要素について、その像の崩壊はその要素に等しい、と。証明は、階層の要素の上の整礎帰納です。

証明は、二方向で外延性によって要素を比較します。

```agda
    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` と同一視します。

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

前者の証人は `r ≺ F m` と等式 `col r ≡ b` からなります。関係の証明を `R→Pre` で読み戻すと、`r` と `F m` のファイバーが得られます。その添字は対応する `μ` の提示要素を示し、最後の成分はそれらの間の所属を記録します。

```agda
           → ⟨ 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
```

`F m` 上のファイバーは命題なので、関係の証明から得た代表 `q` は明らかな代表 `(m , refl)` と等しくなります。この等式に沿って輸送すると、読み取った所属は、前者の添字が `m` の表す集合に属すという主張になります。

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

等式 `⟪ μ ⟫↪ m ≡ v` を使うと、この所属は前者の表す集合を周囲の所属における `v` の下に置きます。したがって、その前者で再帰の仮定を使い、その崩壊値を提示された集合と同一視できます。

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

帰納の仮定は、復号された添字の崩壊値を、その添字が表す要素と同一視します。ファイバーの等式はさらに、その添字の像を `r` と同一視します。そこで `col` の合同性を使うと、提示要素と `col r` の間の必要な等式が得られ、これを `col r ≡ b` と合成すれば順方向の包含が完了します。

```agda
          cpr = sym ih ∙ cong col (snd p)
```

次に逆方向の包含を示します。`b` が添字 `m` の表す集合に属すると仮定し、`b ∈ col (F m)` を目指します。まず順序数 `μ` の推移性により `b` は `μ` の要素でもあるので、`μ` の正準な提示から `b` を表す添字 `k` が得られます。

```agda
      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` を返します。小所属 `_∈ₛ_` が正準な提示の命題値ファイバーに基づくためです。これはその提示に対する局所的な逆操作であり、任意の切り詰められた存在からの選択ではありません。

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

`fiber` が返す等式により、もとの所属 `b ∈ ⟪ μ ⟫↪ m` を、提示要素 `⟪ μ ⟫↪ k` の所属として書き換えられます。そこで、明らかな二つのファイバー `(k , refl)`、`(m , refl)` とこの所属から `PreT (F k) (F m)` が得られます。

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

この `PreT` の事実を Bool 関係に符号化すると `F k ≺ F m` が得られます。したがって、崩壊の導入則により `col (F k)` は `col (F m)` に属します。同時に、提示要素が `m` の表す集合に属すことから、それは帰納の引数 `v` より下にあるので、再帰の仮定を `k` に適用できます。

```agda
        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)` へ輸送すれば、逆方向の包含が完了します。

```agda
                  (∈∈ₛ {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` を導きます。この時点ではまだその包含を主張していません。

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

`μ` の各要素 `b` は崩壊像 `ot` にも属します。`b` における `μ` の正準なファイバーから、`⟪ μ ⟫↪ m ≡ b` を満たす添字 `m` が得られます。補題 `key'` はこの代表を `col (F m)` と同定し、`ot-in` はその崩壊値を `ot` に入れます。二つの等式に沿って輸送すれば `b ∈ ot` が得られます。

したがって、ここで示されるのは包含 `μ ⊆ ot` だけです。これと `ot ∈ μ` を合わせれば矛盾には十分であり、`μ` と `ot` の等しさや順序同型を示す必要はありません。

```agda
    μ⊆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
```

正準な提示のファイバーは命題なので、`b` に対して復元される代表は一意に定まります。その代表と等式をまとめて `fb` として保持することで、直前の包含証明における `key'` と `ot-in` の両方に必要な添字が得られます。

```agda
      fb = fiber μ b∈μ
```

上界の構成により、`ot` は `μ` の要素です。この要素に包含 `μ ⊆ ot` を適用すると `ot ∈ ot` が得られ、所属関係の非反射性に反します。これで、仮定した単射 `μ ↪ a` から生じる矛盾が完成します。

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

上の局所的な矛盾は、任意の単射 `f : ⟪ μ ⟫ ↪ ⟪ a ⟫` を仮定して証明されました。定理 `noInj` はこの結論を Hartogs モジュールの外部へ提示します。どの単射を仮定しても、上で用いた引き戻し関係が得られ、したがって `Empty.⊥` に至ります。

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

## 得られた大きい L 基数

各順序数 `x` に対して、明示的な対象 `Hartogs.μ x` は順序数であり、`x` への単射を持ちません。この対象、その順序数性、単射が存在しないことの三つを命題的切り詰めの中に収めると、`NoInjOrd` が得られます。したがって、包装する前には定まった証人があり、呼び出し側が受け取るのはその切り詰められた存在だけです。

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

最後に、`noInjOrd→CardAboveLᵀ` は Hartogs の証人から真に大きい周囲の順序数基数を作り、その順序数を `L` に入れ、周囲での基数性を内部の基数性へ移します。得られる存在は命題的に切り詰められています。すなわち、与えられた順序数基数 `κ` に対して、`κ ∈ θ` を満たす構成可能な内部基数 `θ` が存在します。

この定理は、後の後続基数の構成に必要な候補が空でないことを保証しますが、その最小要素を選びません。`L.GCH.Assembly` が、ここで得た証人によって探索範囲を定めた後に最小化を行います。

```agda
CardAboveL : CardAboveLᵀ
CardAboveL = noInjOrd→CardAboveLᵀ noInjOrd
```