GCH の議論に必要な十分な段階

module At (c : V ℓ) (oc : IsOrd c) where

構成可能段階 Lset c を台 A としてまとめる。この台から、階層表、論理式符号の集合、充足関係のグラフ、環境の塔という四つの証人をそれぞれ構成する。

A : CS.S
A = LsetS c oc

順序数添字 c 自身も構成可能である。ord∈Lset-suc が c を Lset (sucV c) に入れ、順序数で添字づけられた構成可能段階への所属から、必要な構成可能性の証拠 cL が得られる。

cL : ⟨ isL c ⟩
cL = Lset→isL (sucV c) (suc-ord oc) c (ord∈Lset-suc c oc)

最初の証人は c における内部の階層表である。これは L の内部で、順序数添字が c より下にある構成可能段階を記録する。

hier : CS.S
hier = hierL c cL oc

第二の証人は、段階の台の上のすべての論理式符号からなる集合である。これらの符号は、後の階層記述で使われる。

codes : CS.S
codes = AllCodes A

一様な充足の表の順序対のグラフが第三の証人である。それぞれのキーに割り当てられた値を記録する。

table : CS.S
table = SatGraph.pairs A

環境の塔が第四の証人である。すべての有限の長さの環境を集める。

tower : CS.S
tower = Tower.tower A

module Adequate (γ : V ℓ) (ad : Adequate γ) where

ord = ad .fst
succ = ad .snd .fst
ω∈ = ad .snd .snd .fst
wit = ad .snd .snd .snd

module Bound1 (α : V ℓ) (oα : IsOrd α) where

まとめられた各構成可能集合 s : CS.S には、誕生段階の添字 stage (s .fst) (s .snd) がある。この補助式は、α の提示された一要素という文脈の中で、この操作を記録する。得られる添字は証人集合 s に依存し、周囲の引数は、その証人がどの要素について作られたかを記録する。

private
  W : ⟪ α ⟫ → (c : V ℓ) → IsOrd c → CS.S → V ℓ
  W m c oc s = stage (s .fst) (s .snd)

α の提示されたすべての要素は順序数である。順序数の要素は順序数だからである。

  oc : (m : ⟪ α ⟫) → IsOrd (ι α m)
  oc m = mem-ord {A = α} oα (ι α m) (ι∈ α m)

st を四つの証人構成にそれぞれ適用すると、誕生段階の添字からなる四つの族が得られる。次の共通上界は、これら四つの族を厳密に上から抑える必要がある。

  st : (f : (c : V ℓ) (o : IsOrd c) → CS.S) → ⟪ α ⟫ → V ℓ
  st f m = stage ((f (ι α m) (oc m)) .fst) ((f (ι α m) (oc m)) .snd)

誕生段階の添字 st f m は順序数である。これは誕生段階の構成に関する一般定理 stage-ord を、証人の基礎となる集合とその構成可能性の証拠に適用して得られる。

  st-ord : (f : (c : V ℓ) (o : IsOrd c) → CS.S) (m : ⟪ α ⟫) → IsOrd (st f m)
  st-ord f m = stage-ord ((f (ι α m) (oc m)) .fst) ((f (ι α m) (oc m)) .snd)

ここで五つの厳密な共通上界を取る。最初の四つは、α の提示された各要素について、階層表、符号集合、充足グラフ、環境の塔の誕生段階の添字をそれぞれ上から抑える。五つ目は、順序数の後続 sucV (ι α m) 自身を上から抑える。これらは順序数添字の間の上界であり、五つ目の族は誕生段階の族ではない。

  b1 = boundingOrd ⟪ α ⟫ (st At.hier) (st-ord At.hier)
  b2 = boundingOrd ⟪ α ⟫ (st At.codes) (st-ord At.codes)
  b3 = boundingOrd ⟪ α ⟫ (st At.table) (st-ord At.table)
  b4 = boundingOrd ⟪ α ⟫ (st At.tower) (st-ord At.tower)
  b5 = boundingOrd ⟪ α ⟫ (λ m → sucV (ι α m)) (λ m → suc-ord (oc m))

六つ目の厳密な上界は、出発点の添字 α と ω の両方を含む。次に二項上界で六つの要請をまとめる。b7 は最初の二つの証人上界を、b8 は残る二つを、b9 は後続の上界と α および ω の上界を、b10 は四つの証人上界をそれぞれまとめる。最小の上界であるとは主張しない。これらの操作が与えるのは、必要な所属証明を伴う厳密な共通上界である。

  b6 = bound2 α ω oα ω-ord
  b7 = bound2 (b1 .fst) (b2 .fst) (b1 .snd .fst) (b2 .snd .fst)
  b8 = bound2 (b3 .fst) (b4 .fst) (b3 .snd .fst) (b4 .snd .fst)
  b9 = bound2 (b5 .fst) (b6 .fst) (b5 .snd .fst) (b6 .snd .fst)
  b10 = bound2 (b7 .fst) (b8 .fst) (b7 .snd .fst) (b8 .snd .fst)

最後の二項上界は、後者、α、ω を担う枝と、四種類の誕生段階の上界を担う枝とを合わせる。したがって、その第一成分は六種類の要請すべてを同時に厳密に上から抑える。

  b11 = bound2 (b9 .fst) (b10 .fst) (b9 .snd .fst) (b10 .snd .fst)

最終上界の第一成分を、新しい順序数添字 β とする。これは V ℓ の中の添字であり、証人を収める構成可能段階は Lset β である。

β : V ℓ
β = b11 .fst

最終の上界は順序数である。二項の上界の操作によって順序数から作られたからである。

oβ : IsOrd β
oβ = b11 .snd .fst

最後の合成に供給された二つの部分的な上界は、最終の上界の下にある。

private
  b9∈ : ⟨ b9 .fst ∈ β ⟩
  b9∈ = b11 .snd .snd .fst
  b10∈ : ⟨ b10 .fst ∈ β ⟩
  b10∈ = b11 .snd .snd .snd

β は推移的なので、厳密な所属を上界の木に沿って下へ伝えられる。b9 ∈ β から、後続の上界 b5 ∈ β と、α および ω の共通上界 b6 ∈ β が得られる。また b10 ∈ β から、まず b7 ∈ β が得られる。

  b5∈ : ⟨ b5 .fst ∈ β ⟩
  b5∈ = tr β oβ (b9 .fst) (b5 .fst) b9∈ (b9 .snd .snd .fst)
  b6∈ : ⟨ b6 .fst ∈ β ⟩
  b6∈ = tr β oβ (b9 .fst) (b6 .fst) b9∈ (b9 .snd .snd .snd)
  b7∈ : ⟨ b7 .fst ∈ β ⟩

もう一方の枝から b8 ∈ β が得られる。さらに b7 を一段下ると、最初の証人上界 b1 も β に属する。同じ推移性の議論を繰り返せば、残る各証人上界も β に入る。

  b7∈ = tr β oβ (b10 .fst) (b7 .fst) b10∈ (b10 .snd .snd .fst)
  b8∈ : ⟨ b8 .fst ∈ β ⟩
  b8∈ = tr β oβ (b10 .fst) (b8 .fst) b10∈ (b10 .snd .snd .snd)
  b1∈ : ⟨ b1 .fst ∈ β ⟩
  b1∈ = tr β oβ (b7 .fst) (b1 .fst) b7∈ (b7 .snd .snd .fst)

第二と第三の証人上界 b2 と b3 は、それぞれ枝 b7 と b8 から得られる。第四の上界 b4 も b8 の下で同じ位置にあるので、次の行でこの対称な議論が完結する。

  b2∈ : ⟨ b2 .fst ∈ β ⟩
  b2∈ = tr β oβ (b7 .fst) (b2 .fst) b7∈ (b7 .snd .snd .snd)
  b3∈ : ⟨ b3 .fst ∈ β ⟩
  b3∈ = tr β oβ (b8 .fst) (b3 .fst) b8∈ (b8 .snd .snd .fst)
  b4∈ : ⟨ b4 .fst ∈ β ⟩

証人側の枝を最後に一段下ると b4 ∈ β が得られる。これで、四つの誕生段階の上界すべてが、共通の順序数添字 β に厳密に属することが分かった。

  b4∈ = tr β oβ (b8 .fst) (b4 .fst) b8∈ (b8 .snd .snd .snd)

b6 を通る枝は、出発点の順序数添字も保つ。α ∈ b6 と b6 ∈ β から、推移性により α ∈ β が得られる。

α∈β : ⟨ α ∈ β ⟩
α∈β = tr β oβ (b6 .fst) α b6∈ (b6 .snd .snd .fst)

同じ枝は ω も保つ。ω ∈ b6 に b6 ∈ β をつなぐと、後で必要となる ω ∈ β が得られる。

ω∈β : ⟨ ω ∈ β ⟩
ω∈β = tr β oβ (b6 .fst) ω b6∈ (b6 .snd .snd .snd)

x ∈ α ならば、提示のファイバーから、ι α m ≡ x を満たす添字 m が得られる。五つ目の共通上界は sucV (ι α m) を含み、b5 ∈ β を経て、それが β に属することが分かる。最後にファイバーの等式に沿って置換し、sucV x ∈ β を得る。したがって、この一回の構成が示す後続閉包は α の要素に対するものだけであり、一回の上界構成に必要な結論と正確に一致する。

suc∈β : (x : V ℓ) → ⟨ x ∈ α ⟩ → ⟨ sucV x ∈ β ⟩
suc∈β x x∈ = subst (λ u → ⟨ sucV u ∈ β ⟩) (fib .snd)
  (tr β oβ (b5 .fst) (sucV (ι α (fib .fst))) b5∈ (b5 .snd .snd (fib .fst)))
  where
  fib : Σ[ m ∶ ⟪ α ⟫ ] (ι α m ≡ x)

∈-asFiber は、周囲の所属の証明からこのファイバーを復元する。ここで得られるのは実際の依存対であり、命題的に切り詰められた存在だけではない。小さな提示は埋め込みを使うため、x の提示添字を同定するファイバーは命題値だからである。

  fib = ∈-asFiber {a = x} {b = α} x∈

共通の順序数上界 β は、四種類の証人の出生段階の添字をすべて厳密に上から押さえるように構成されている。ここから、その証人自身を構成可能段階 Lset β に入れる。

private

四つの証人構成の一つ f と、α の要素を呈示する添字 m を固定する。対応する証人は Lset (st f m) に現れ、その出生添字は記録された上界 b.fst に属し、さらに b.fst は最終上界 β に属する。着地の補題は、ここから得られる Lset β への所属をまとめる。

  land : (f : (c : V ℓ) (o : IsOrd c) → CS.S)
         (b : Σ[ σ ∶ V ℓ ] (IsOrd σ × ((m : ⟪ α ⟫) → ⟨ st f m ∈ σ ⟩)))
       → ⟨ b .fst ∈ β ⟩
       → (m : ⟪ α ⟫) → ⟨ (f (ι α m) (oc m)) .fst ∈ Lset β ⟩
  land f b b∈ m =

内側の Lset-mono は証人を Lset (st f m) から Lset (b.fst) へ運び、外側の適用がさらに Lset β へ運ぶ。どちらの移動も、対応する順序数添字どうしの厳密な所属に基づく。

    Lset-mono {α = β} {β = b .fst} b∈
      (Lset-mono {α = b .fst} {β = st f m} (b .snd .snd m)
        (stage-mem ((f (ι α m) (oc m)) .fst) ((f (ι α m) (oc m)) .snd)))

m が呈示する要素について、まず階層表と論理式コードの集合を Lset β に入れる。呼び出し側は任意の証明 o : IsOrd (ι α m) を与えられるが、順序数性は命題なので、証人の構成に用いた oc m と同一視できる。

  witAt : (m : ⟪ α ⟫) → Witnesses (Lset β) (ι α m)
  witAt m o =
      subst (λ u → ⟨ (At.hier (ι α m) u) .fst ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
        (land At.hier b1 b1∈ m)
    , ( subst (λ u → ⟨ (At.codes (ι α m) u) .fst ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)

同じ議論でコード集合の所属を完成し、充足関係のグラフと環境の塔も Lset β に入れる。これで Witnesses (Lset β) (ι α m) の四成分がすべて得られ、その結果は特定の順序数性証明に依存しない。

          (land At.codes b2 b2∈ m)
      , ( subst (λ u → ⟨ (At.table (ι α m) u) .fst ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
            (land At.table b3 b3∈ m)
        , subst (λ u → ⟨ (At.tower (ι α m) u) .fst ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
            (land At.tower b4 b4∈ m) ))

所属の証明 c ∈ α からは実際の提示ファイバーが得られ、添字 m と等式 ι α m ≡ c が取り出される。その等式に沿って witAt m を輸送すれば、抽象的に指定された要素 c の四つの証人が得られる。ここでは命題的切り詰めの除去も選択も行わない。

wit : (c : V ℓ) → ⟨ c ∈ α ⟩ → Witnesses (Lset β) c
wit c c∈ = subst (Witnesses (Lset β)) (fib .snd) (witAt (fib .fst))
  where
  fib : Σ[ m ∶ ⟪ α ⟫ ] (ι α m ≡ c)
  fib = ∈-asFiber {a = c} {b = α} c∈

module Union (ch : ℕ → V ℓ) (och : (n : ℕ) → IsOrd (ch n)) where

累積階層の合併は、周囲の宇宙レベルにある小さな添字型を要求する。ℕ を Lift ℕ に替えても変わるのは宇宙での位置だけで、F (lift n) は依然として順序数 ch n である。

private
  F : Lift {ℓ-zero} {ℓ} ℕ → V ℓ
  F n = ch (lower n)

この順序数族の集合論的な合併を、順序数添字 γ と書く。この時点で γ は周囲の累積階層の集合であり、対応する構成可能段階は Lset γ である。

γ : V ℓ
γ = ⋃ (sett (Lift {ℓ-zero} {ℓ} ℕ) F)

任意の順序数族の集合論的合併は、再び順序数である。この事実を F に適用して IsOrd γ を得る。ここでは自然数添字の順序や共終性に関する性質を使わない。

oγ : IsOrd γ
oγ = setUnion-ord (Lift {ℓ-zero} {ℓ} ℕ) F (λ n → och (lower n))

内向きの読み出しが、列のそれぞれの項目のすべての要素を、合併の中に受け入れる。

into : (n : ℕ) (x : V ℓ) → ⟨ x ∈ ch n ⟩ → ⟨ x ∈ γ ⟩
into n x = union-family-in (Lift {ℓ-zero} {ℓ} ℕ) F (lift n) x

外向きの読み出しは、切り詰めのもとで、合併の任意の要素を含む列の項目を復元する。切り詰められた添字は、命題の中だけで消費される。

outof : (x : V ℓ) → ⟨ x ∈ γ ⟩ → ∥ Σ[ n ∶ ℕ ] ⟨ x ∈ ch n ⟩ ∥₁
outof x h = map₁ (λ { (n , hn) → lower n , hn })
  (union-family-out (Lift {ℓ-zero} {ℓ} ℕ) F x h)

module Above (p : V ℓ) (op : IsOrd p) where

最初の上界は、出発順序数 p と順序数 ω の両方を厳密に含む順序数である。これにより、最終的な合併まで保つべき二つの所属が直ちに得られる。

private
  base = bound2 p ω op ω-ord

第零の順序数は最初の共通上界である。その後は各順序数を直前の項に Bound1 を適用して作るので、ch n の要素から生じる義務は ch (suc n) で満たされる。一回の構成だけで、その結果自身の全要素について十分になるとは主張していない。

ch : ℕ → Σ[ β ∶ V ℓ ] IsOrd β
ch  = base .fst , base .snd .fst
ch (suc n) = Bound1.β (ch n .fst) (ch n .snd) , Bound1.oβ (ch n .fst) (ch n .snd)

ここで、先の合併構成をこれらの順序数添字に適用する。内向きの写像は既知の所属を合併へ送り、外向きの写像は任意の要素を含む項を命題的切り詰めのもとでのみ位置づける。

module C = Union (λ n → ch n .fst) (λ n → ch n .snd) using (into; outof; oγ; γ)

これらの順序数添字の合併を γ とする。一段階の遅れは合併によって吸収される。ある項に現れた要素について、その後者と四つの証人集合は後の項で処理される。最終的に証人が属すべき先は添字 γ 自身ではなく、Lset γ である。

γ : V ℓ
γ = C.γ

各 ch n が順序数なので、その集合論的合併 γ も順序数である。ここで得られるのは IsOrd γ だけであり、Adequate γ の閉性と証人の成分は以下で別に証明する。

oγ : IsOrd γ
oγ = C.oγ

列のそれぞれの項目は、その後続の項目より厳密に下にある。一段階の上界の所属の条項によるものである。

private
  up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
  up n = Bound1.α∈β (ch n .fst) (ch n .snd)

順序数添字 ch n 自身を合併 γ に入れるには、まず ch n ∈ ch (suc n) を使い、ついで ch (suc n) の各要素を合併へ入れる。この事実が、後で Lset の単調性に必要な添字の比較を与える。

  ch∈γ : (n : ℕ) → ⟨ ch n .fst ∈ γ ⟩
  ch∈γ n = C.into (suc n) (ch n .fst) (up n)

基底の上界はすでに p を含む。これは列の第零項なので、合併の内向きの写像がこの所属を保ち、p ∈ γ を与える。

p∈γ : ⟨ p ∈ γ ⟩
p∈γ = C.into zero p (base .snd .snd .fst)

同じ内向きの写像が ω ∈ ch 0 を ω ∈ γ へ送る。これが Adequate γ に必要な所属の成分である。

ω∈γ : ⟨ ω ∈ γ ⟩
ω∈γ = C.into zero ω (base .snd .snd .snd)

x ∈ γ が与えられると、外向きの写像は x ∈ ch n を満たす添字 n の命題的に切り詰められた存在だけを与える。切り詰めの各分岐では、次の Bound1 が sucV x を ch (suc n) に入れ、そこから γ に入れる。目標の所属 sucV x ∈ γ は命題なので、各分岐を再びまとめられる。特定の n が命題的切り詰めの外へ取り出されることはない。

succ : (x : V ℓ) → ⟨ x ∈ γ ⟩ → ⟨ sucV x ∈ γ ⟩
succ x x∈ = rec₁ ((sucV x ∈ γ) .snd)
  (λ { (n , x∈n) → C.into (suc n) (sucV x) (Bound1.suc∈β (ch n .fst) (ch n .snd) x x∈n) })
  (C.outof x x∈)

c ∈ γ に対しても、外向きの写像が与えるのは c ∈ ch n を満たす n の命題的に切り詰められた存在だけである。各分岐では、一段階の上界構成が四つの証人を Lset (ch (suc n)) に用意し、ch (suc n) ∈ γ に沿う Lset-mono がそれらを Lset γ へ運ぶ。Witnesses (Lset γ) c は命題なので、得られた結果を命題的切り詰めから除去できる。

wit : (c : V ℓ) → ⟨ c ∈ γ ⟩ → Witnesses (Lset γ) c
wit c c∈ = rec₁ (isPropWitnesses (Lset γ) c)
  (λ { (n , c∈n) → λ oc →
    let w = Bound1.wit (ch n .fst) (ch n .snd) c c∈n oc
        mono = Lset-mono {α = γ} {β = ch (suc n) .fst} (ch∈γ (suc n))

写像 mono は、添字 ch (suc n) から添字 γ への構成可能階層の単調性を表す。これを階層表、コード集合、充足関係のグラフ、環境の塔にそれぞれ適用して、四成分の証人を完成する。

    in mono (w .fst) , ( mono (w .snd .fst) , ( mono (w .snd .snd .fst) , mono (w .snd .snd .snd) )) })
  (C.outof c c∈)

順序数添字 γ は、ここで Adequate の四つの条項をすべて満たす。すなわち、順序数性、後者閉包、ω の所属、そして各 c ∈ γ に対応する四つの証人を、添字とは別の構成可能段階 Lset γ に入れることである。後で使う妥当性の内容は、この四項目に尽きる。

adequate : Adequate γ
adequate = oγ , ( succ , ( ω∈γ , wit ))

module Super (α : V ℓ) (oα : IsOrd α) where

第零項は adequate-above α oα が明示的に返す順序数添字である。この添字は十分であり、出発順序数 α を厳密に含む。これらの事実は後で使えるよう項とともに保持される。

ch : ℕ → Σ[ γ ∶ V ℓ ] (IsOrd γ × Adequate γ)
ch  =
  adequate-above α oα .fst
  , ( adequate-above α oα .snd .fst , adequate-above α oα .snd .snd .snd )
ch (suc n) =

十分な順序数添字 ch n にもう一度 adequate-above を適用すると、次の十分な添字 ch (suc n) と所属 ch n ∈ ch (suc n) が得られる。この定理はそのような次の添字を明示的に与えるが、最小性は主張しない。

  adequate-above (ch n .fst) (ch n .snd .fst) .fst
  , ( adequate-above (ch n .fst) (ch n .snd .fst) .snd .fst
    , adequate-above (ch n .fst) (ch n .snd .fst) .snd .snd .snd )

この十分な順序数添字の列に合併構成を適用する。先ほどと同様、合併の要素をある項に位置づけられるのは命題的切り詰めのもとだけである。

module U = Union (λ n → ch n .fst) (λ n → ch n .snd .fst) using (into; outof; oγ; γ)

これらの順序数添字の合併を、コードでは lam、本文では λ と書く。以下で示すのは、順序数添字 λ が Adequate λ と Superadequate λ の両方を満たすことである。対応する構成可能段階 Lset λ は、証人の条項でのみ使われる。

lam : V ℓ
lam = U.γ

各 ch n が順序数なので、その集合論的合併 λ も順序数である。この議論から、より強い極限性、正則性、基数としての性質は導かれない。

olam : IsOrd lam
olam = U.oγ

列のそれぞれの項目は、その後続の項目より厳密に下にある。adequate-above が産出する厳密な所属によるものである。

private
  up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
  up n = adequate-above (ch n .fst) (ch n .snd .fst) .snd .snd .fst

ch n ∈ ch (suc n) なので、合併の内向きの写像から ch n ∈ λ が得られる。したがって、列にある各十分な添字自身が最終的な順序数添字 λ の要素として利用できる。

  ch∈λ : (n : ℕ) → ⟨ ch n .fst ∈ lam ⟩
  ch∈λ n = U.into (suc n) (ch n .fst) (up n)

第零の十分な添字は α を厳密に含み、しかも合併を構成する集合の一つである。したがって α ∈ λ が従う。

α∈λ : ⟨ α ∈ lam ⟩
α∈λ = U.into zero α (adequate-above α oα .snd .snd .fst)

x ∈ λ が与えられると、外向きの写像が与えるのは x ∈ ch n を満たす n の命題的に切り詰められた存在だけである。各分岐では、その項の妥当性から sucV x ∈ ch n が得られ、内向きの写像が sucV x ∈ λ を与える。目標は所属命題なので、n を保持せずに結果を命題的切り詰めから除去できる。

succ : (x : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ sucV x ∈ lam ⟩
succ x x∈ = rec₁ ((sucV x ∈ lam) .snd)
  (λ { (n , x∈n) → U.into n (sucV x) (Adequate.succ (ch n .fst) (ch n .snd .snd) x x∈n) })
  (U.outof x x∈)

第零項は十分なので ω を含む。合併の内向きの写像がこの事実を、Adequate λ に必要な所属 ω ∈ λ へ送る。

ω∈λ : ⟨ ω ∈ lam ⟩
ω∈λ = U.into zero ω (Adequate.ω∈ (ch zero .fst) (ch zero .snd .snd))

c ∈ λ に対し、外向きの写像が与えるのは c ∈ ch n を満たす n の命題的に切り詰められた存在だけである。各分岐では、ch n の妥当性が四つの証人を Lset (ch n) に与え、ch n ∈ λ に沿う単調性がそれらを Lset λ へ運ぶ。Witnesses (Lset λ) c は命題なので、命題的切り詰めから正当に除去できる。

wit : (c : V ℓ) → ⟨ c ∈ lam ⟩ → Witnesses (Lset lam) c
wit c c∈ = rec₁ (isPropWitnesses (Lset lam) c)
  (λ { (n , c∈n) → λ oc →
    let w = Adequate.wit (ch n .fst) (ch n .snd .snd) c c∈n oc
    in  Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .fst)

各成分は ch n ∈ λ に沿う構成可能段階の単調性によって運ばれる。階層表、コード集合、充足関係のグラフ、環境の塔はいずれも Lset (ch n) から Lset λ へ移る。

      , ( Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .fst)
        , ( Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .snd .fst)
          , Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .snd .snd) )) })
  (U.outof c c∈)

合併の順序数性、後者閉包、ω ∈ λ、そして輸送した証人を組み合わせると Adequate λ が得られる。最初の三項は順序数添字 λ に関する事実であり、第四項は集合を構成可能段階 Lset λ に入れる。これらは後の階層記述が使う閉包の事実であり、Lset λ に関するモデル理論的な主張ではない。

adequate : Adequate lam
adequate = olam , ( succ , ( ω∈λ , wit ))

d ∈ λ に対し、外向きの写像が与えるのは d ∈ ch n を満たす n の命題的に切り詰められた存在だけである。その切り詰めの内部で γ = ch n と置けば、この添字は λ に属し、d を含み、十分である。結果は切り詰められたままなので、選択関数 d ↦ γ は定義されない。

super : Superadequate lam
super d d∈ = map₁
  (λ { (n , d∈n) → ch n .fst , ( ch∈λ n , ( d∈n , ch n .snd .snd )) })
  (U.outof d d∈)