---
title: "符号化された対に沿う階数降下"
module: L.Coding.Descent
lang: ja
site: "Bedrock"
description: "符号化された対に沿う階数降下"
stage: "内部の符号化：式と定義域"
reading_order: 45
canonical: https://bedrock.institute/ja/L.Coding.Descent.html
html: L.Coding.Descent.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Descent.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Coding, L.Rank]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Descent.md, https://bedrock.institute/zh/L.Coding.Descent.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 符号化された対に沿う階数降下

```agda
open import Base.Prelude
```

宇宙レベル `ℓ` を固定する。このレベルをパラメータとして保つことで、異なる宇宙を同一視せずに、必要な大きさで構成を具体化できる。

```agda
module L.Coding.Descent {ℓ : Level} where
```

```agda
open import FOL.ZFStructure using ( module hPropView )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Rank {ℓ} using ( rank; rank-mono; rank-ord )
```

後では符号に対して整礎再帰を行い、各段階で与えられた符号の直下の成分を処理する。再帰が整礎であるためには、符号からその成分へと狭義に減少する尺度が必要である。所属関係はそれを与えてくれない。Kuratowski 対は `pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆` と定義されるので、`b` のような成分に届くには、中間の非順序対 `⁅ a , b ⁆` を経なければならず、この中間集合そのものは符号ではない。したがって所属に関する帰納は、符号についての仮定をそれらの間へ運ぶことができない。

階数ならできる。階数は所属に沿って狭義に増加し、その値は順序数であり、順序数の所属は推移的である。そこで有限の所属の連鎖は一つの順序数の比較へと縮み、再帰は符号そのものではなく**階数**に関する整礎帰納によって正当化できる。本章が組み立てるのはまさにこの比較である。順序対の各側ごとに一段階、さらにそれを合成して、対になったペイロードの各側から外側のタグ付き符号への 4 段階の降下を得る。

数学的な舞台は累積階層である。その台 `S`、命題値をとる所属 `∈ˢ`、そして集合論的演算をひとまとめにした構造 `𝒮ᵥ` である。降下を証明する前に一つ、準備をはっきりさせておく。整礎再帰には狭義の尺度が必要で、後で使う尺度は von Neumann の階数である。これはランクの章で定義され研究されている。そこでは `rank-mono` が階数が所属に沿って狭義に増加することを、`rank-ord` がすべての階数が順序数であることを記録している。

具体的な難しさは符号の形から読み取れる。`pr a b` の成分は `pr a b` の直接の要素ではない。それは非順序対 `⁅ a , b ⁆` の中に包まれ、後者はさらに外側の非順序対の 2 つの要素の一つである。所属が与えるのは 1 本の辺ではなく複数段階の連鎖であり、連鎖の環となる集合はまったく符号の構造を持たないものである。この連鎖の代わりとなるのが、各所属の辺を階数を通して翻訳し、それを合成して得られる順序数どうしの狹義の不等式である。

この比較には階層からの 3 つの材料を使う。非順序対 `⁅ u , v ⁆`、非順序対への所属を命題として特徴づける対の公理 `pairing-ax`、そして根底の集合としての所属と構造化された所属 `∈ˢ` とを相互に変換する `∈∈ₛ` である。和型 `_⊎_` は 2 つの成分の明示的な選択を運ぶ。左には `inl`、右には `inr` である。ここで選択を「単に存在する」ではなく明示的に保つことが重要なのは、降下の証明が対のどちらの成分へ降りるのかを指摘しなければならないからである。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s )
```

重要なのは、推移性を使える場所の区別である。任意の集合の所属を推移的とはみなしない。各所属の辺を `rank-mono` で階数どうしの関係へ移した後にはじめて、中間の対象が順序数となり、`rank-ord` がその狭義の不等式を合成するための推移性を与える。

```agda
open hPropView 𝒮ᵥ
```

## 階数を下げる基本段階

降下の議論は 2 つの再利用可能な事実に立っている。第 1 は非順序対への所属の辺である。`w` が `u` か `v` に明示的に等しいなら、`w` は `⁅ u , v ⁆` に属する。第 2 は階数の段階である。1 本の所属の辺 `x ∈ˢ y` と `y` から `z` への階数降下があれば、`x` から `z` への階数降下が得られる。両者を合わせると、所属の連鎖が一つの順序数の比較に変わる。しかも任意の集合について成り立ち、特定の対の式に限定されない。

対の公理は `⁅ u , v ⁆` の所属を切り詰められた選言として特徴づける。「要素が `u` に等しいか `v` に等しい」という選言全体が切り詰められている。補題 `pair∈` は、切り詰めを外した逆向きを与える。明示的な和 `w ≡ u ⊎ w ≡ v` を受け取り、`∣ h ∣₁` を `pairing-ax` の切り詰められた側に挿入し、`∈∈ₛ` で変換して、`⟨ w ∈ˢ ⁅ u , v ⁆ ⟩` の証明を返す。これがまさに降下の証明に必要な方向である。どちらの成分へ降りるかが指摘されていれば、場合分けなしに所属が従う。合成の段階 `trans≺` が次に階数への翻訳を行う。`rank-ord z` により `rank z` は順序数であり、`rank z` の下での所属は推移的なので、`rank x ∈ˢ rank y` と `rank y ∈ˢ rank z` は `rank x ∈ˢ rank z` に合成される。第 1 の仮定は `x ∈ˢ y` に `rank-mono x y` を施したものである。推移性を使うのは順序数としての階数についてであって、任意の集合の所属について推移性を仮定することは決してない、と注意してほしい。

```agda
pair∈ : (u v w : S) → (w ≡ u) ⊎ (w ≡ v) → ⟨ w ∈ˢ ⁅ u , v ⁆ ⟩
pair∈ u v w h = ∈∈ₛ {a = w} {b = ⁅ u , v ⁆} .snd (pairing-ax u v w .snd ∣ h ∣₁)

trans≺ : (x y z : S) → ⟨ x ∈ˢ y ⟩ → ⟨ rank y ∈ˢ rank z ⟩ → ⟨ rank x ∈ˢ rank z ⟩
trans≺ x y z x∈y ry∈rz = rank-ord z .fst (rank-mono x y x∈y) ry∈rz
```

## タグ付きコードのペイロードへ降りる

2 つの基本段階が手もとにあれば、符号化された対の降下は Kuratowski 対の形を読むだけで得られる。`pr a b` の成分 `x` が符号全体に届くには 2 本の所属の辺を経る。`x` は `⁅ a , b ⁆` に属し、`⁅ a , b ⁆` は `pr a b` に属する。そこで `pair-component≺` は任意の成分についてこの 2 段階の降下を証明し、タグには何の条件も課さない。第 2 成分に限定すると `payload≺`、すなわちペイロードからそのタグ付き符号への降下が得られる。タグ `c` のもとの対になったペイロード `pr a b` にはもう一度の合成が要るが、ここで両側は実際に異なる。`leftPart` はまずペイロードの内側の第 1 成分へ降り、それからペイロード降下と合成する。`rightPart` はペイロード降下を 2 回施すだけである。通じてタグ `c` は任意の集合であり、数項である必要も、そこへ降りることもない。

2 本の辺は明示的に供給される。第 1 は与えられた選択 `h : x ≡ a ⊎ x ≡ b` を `pair∈ a b x h` で使う。第 2 の選択は `inr refl` である。非順序対 `⁅ a , b ⁆` は定義的に外側の対の右の要素なので、`pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl)` がその所属を証明し、`rank-mono` がそれを階数の不等式 `rank ⁅ a , b ⁆ ∈ˢ rank (pr a b)` に変える。そして `trans≺` が両者を合成する。途中の集合 `⁅ a , b ⁆` がこの証明の内部にしか現れないことに注意してほしい。`pair-component≺` の命題は符号と選ばれた成分以外に何も言及しない。特殊化 `payload≺` は再び `inr refl` によって `z` を `pr c z` の右成分と読み、任意のタグ `c` に対するペイロードからそのタグ付き符号への降下を与える。

```agda
pair-component≺ : (a b x : S) → (x ≡ a) ⊎ (x ≡ b) → ⟨ rank x ∈ˢ rank (pr a b) ⟩
pair-component≺ a b x h = trans≺ x ⁅ a , b ⁆ (pr a b) (pair∈ a b x h)
  (rank-mono ⁅ a , b ⁆ (pr a b) (pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl)))

payload≺ : (c z : S) → ⟨ rank z ∈ˢ rank (pr c z) ⟩
payload≺ c z = pair-component≺ c z z (inr refl)
```

タグのもとの両補題は、順序数 `rank (pr c (pr a b))` において合成される。使うのは `rank-ord` の推移性のフィールドである。両者の非対称性は入れ子の構造を反映している。`leftPart` では目標 `a` はペイロードの内側の第 1 成分なので、第 1 の辺は `pair-component≺ a b a (inl refl)` で、`rank a ∈ˢ rank (pr a b)` を与える。第 2 の辺はペイロード降下 `payload≺ c (pr a b)` である。`rightPart` では目標 `b` はペイロード自身の第 2 成分なので、両方の辺がペイロード降下である。`payload≺ a b` が `b` から `pr a b` へ、次に `payload≺ c (pr a b)` がペイロードから外側のタグ付き符号へ。どちらの場合も結論は同じ形、`rank a` または `rank b` が `rank (pr c (pr a b))` に属する、であり、これは後のタグ付き符号上の整礎再帰が各直下の成分に要求する尺度の減少そのものである。

```agda
leftPart : (c a b : S) → ⟨ rank a ∈ˢ rank (pr c (pr a b)) ⟩
leftPart c a b = rank-ord (pr c (pr a b)) .fst
  (pair-component≺ a b a (inl refl)) (payload≺ c (pr a b))

rightPart : (c a b : S) → ⟨ rank b ∈ˢ rank (pr c (pr a b)) ⟩
rightPart c a b = rank-ord (pr c (pr a b)) .fst (payload≺ a b) (payload≺ c (pr a b))
```