四つの内部上界から GCH を組み立てる

この仮定を、証明に必要なただ一つの宇宙レベルで固定する。したがって、最小候補の議論を含む以下の構成は、すべて同じ明示的な実例 LEM (ℓ-suc ℓ) だけに依存する。

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

本章では、L の内部で採用する形の GCH を完成させる。無限な内部順序数基数 κ ごとに、外側の命題的切り詰めのもとで、後続基数 δ と二つの符号化された単射 𝒫κ ↪ δ および δ ↪ 𝒫κ が存在することを示す。証明では切り詰められた枝の内部で証人を使えるが、特定の δ も、どちらの単射のグラフも外へ取り出さない。

組み立てで用いる古典的原理は排中律だけである。候補を小さな整列順序の中に置いた後、単に要素をもつ候補族から一意な最小元を得るために使う。

ここでは、集合論に関する二つの見方を結び付ける。周囲の累積階層は所属と小さな提示を与え、構成可能な部分宇宙は述語 isL と各段階 Lset α を与える。内部の冪集合は、後で ZF モデルの構造によって解釈される。

最小化の議論では、順序数について三つの事実を使う。順序数の所属は推移的であり、任意の二つの順序数には三岐性が成り立ち、順序数の小さな提示上の所属順序は整列順序である。これにより、有界な探索で得た最小候補が、任意の競合する基数を制御できる。

内部の大きさの比較は InjL で表す。これは、単射を符号化する構成可能なグラフが存在するという命題的切り詰めである。IsCardinalL はこの比較から内部の基数を定義し、SuccCardL は与えられた基数より真に大きい最小の内部順序数基数を指定する。一方、CardAboveL が与えるのは、切り詰めの内側にある何らかのより大きい基数だけである。

最終的な GCH の主張は、後続基数が単に存在し、それとモデルの冪集合との間に両方向の符号化された単射があることを要求する。冪集合から出る向きの比較を構成するため、まず包含を単射として符号化し、次に構成可能な段階を数える単射と合成する。

有界探索には、順序数 sucV (θ .fst) の小さな提示を使う。その添字は sucV (θ .fst) の要素、すなわち θ 以下の順序数を表す。一方、ω は考察する基数が有限順序数でないことを表すために使う。二つの構成可能な対の底の集合が等しいとき、構成可能性が命題であることにより、その等しさを対そのものの等しさへ持ち上げられる。

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

三岐性は、直和の三つの分岐に分けて調べる。不可能な分岐は空型に帰着し、命題的切り詰めは選ばれた証人を外へ出さずに存在だけを記録する。したがって、以下での消去先は、所属や別の切り詰められた存在命題のような命題に限られる。

_∈ˢ_ と書く所属は、累積階層における周囲の所属である。点ごとの包含、特に「κ の構成可能な部分集合の各周囲要素が κ にも属する」という主張には、この関係を使う。

open hPropView 𝒮ᵥ using ( _∈ˢ_ )

周囲の命題値の集合論的構造を SV と書く。その台は、点ごとの部分集合の仮定が量化するすべての集合を含む。

module SV = hPropView 𝒮ᵥ

構成可能な集合に制限した対応する構造を SL と書く。その要素は、周囲の底の集合と、その集合が L に属することの証明との対である。

module SL = hPropView 𝒮ʟ

SL 上の ZF モデルの構造は、指定された内部の冪集合 𝒫κ を与える。したがって、以下でいう冪集合はすべて構成可能モデルの冪集合であり、累積階層全体における周囲の冪集合ではない。

module ModelL = FOL.ZFModel 𝒮ʟ

四つの内部評価

最初のインターフェースは、段階が数え上げられるとは何を意味するかを述べる。構成可能な順序数 δ と、底の集合が段階 Lset δ と等しい集合 Lδ の対に対して、δ が有限でなければ、段階から順序数への単射が存在する、というものである。この型は有限の順序数を排除し、符号化された単射の切り詰められた存在だけを産み出す。

StageCountedCoded : Type (ℓ-suc ℓ)
StageCountedCoded =
    (δ Lδ : SL.S) → IsOrd (δ .fst) → (⟨ δ .fst ∈ˢ ω ⟩ → ⊥₀)
  → Lδ .fst ≡ Lset (δ .fst) → InjL Lδ δ

第二のインターフェースは、有界部分集合の定理を述べる。有限ではなく順序数であり内部の基数である κ と、その周囲の要素がすべて κ に属する構成可能な集合 y に対して、単に、順序数 β が存在し、y が段階 Lset β の中にあり、β が κ へ単射する。部分集合の仮定は周囲の集合の上で量化するので、自分自身の構成可能性の証明をもたない要素も覆う。

InternalBoundedSubset : Type (ℓ-suc ℓ)
InternalBoundedSubset =
    (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → (y : SL.S) → ((z : SV.S) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ κ .fst ⟩)
  → ∥ Σ[ β ∶ SL.S ]

産み出される記録には、β の順序数性、y の段階への着地、そして β から κ への符号化された単射が含まれる。

       (IsOrd (β .fst) × ⟨ y .fst ∈ˢ Lset (β .fst) ⟩ × InjL β κ) ∥₁

第三のインターフェースは条件つきの逆向きの比較である。κ の内部の冪集合が κ の後続基数 δ へ単射することが与えられたとき、δ から冪集合への単射を返す。仮定は本当に条件つきであり、後続基数の記録だけから呼び出すことはできない。

SuccIntoPower : ModelL.isZFModel → Type (ℓ-suc ℓ)
SuccIntoPower zf =
    (κ δ : SL.S) → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀) → SuccCardL δ κ
  → InjL (𝒫 κ) δ → InjL δ (𝒫 κ)
  where open ModelL.isZFModel zf using ( 𝒫 )

第四のインターフェースは、後続基数の単なる存在を述べる。無限の内部順序数基数ごとに、ある後続基数が存在する。結論は切り詰められており、呼び出し側がそこから大域的な代表を選ぶことはできない。

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

より大きな内部基数の存在

約簡のモジュールは、κ より真に大きい順序数の内部基数 θ を固定し、θ の後続が決める小さな探索空間の中で、κ より上の最小の基数が存在することを示す。これがこの章の中心である。まず明示的な上界を固定し、その中で最小化するのである。

module Reduce (κ : SL.S) (oκ : IsOrd (κ .fst))
              (θ : SL.S) (oθ : IsOrd (θ .fst))
              (cθ : IsCardinalL θ) (κ∈θ : ⟨ κ .fst ∈ˢ θ .fst ⟩) where

open LeastCardInjL θ oθ using ( up; self; self-eq )

A : Type ℓ
A = ⟪ sucV (θ .fst) ⟫

opaque
  w : SWO A
  w = ordSWO (sucV (θ .fst)) (suc-ord oθ)

opaque
  unfolding w
  w-lt : (m n : A) → let module W = SWO w in (m W.<∙ n)
       ≡ ⟨ ⟪ sucV (θ .fst) ⟫↪ m ∈ˢ ⟪ sucV (θ .fst) ⟫↪ n ⟩
  w-lt m n = refl

isPropIsCardinalL : (x : SL.S) → isProp (IsCardinalL x)
isPropIsCardinalL x =
  isPropΠ (λ _ → isPropΠ (λ _ → isPropΠ (λ _ → isProp⊥)))

Good : A → hProp (ℓ-suc ℓ)
Good b = (IsCardinalL (up b) × ⟨ κ .fst ∈ˢ (up b) .fst ⟩)
       , isProp× (isPropIsCardinalL (up b)) ((κ .fst ∈ˢ (up b) .fst) .snd)

definedGood : FOL.Semantics.FormulaPredicate 𝒮ʟ A SL.S id Good
definedGood = FOL.Semantics.presented 
  (cardinalAt zero ∧̇ (var (suc zero) ∈̇ var zero)) (λ b → up b ∷ κ ∷ [])
  (λ b → ⇔toPath
    (λ { (card , mem) → CardinalAt.fill zero (up b ∷ κ ∷ []) card , mem })
    (λ { (sat , mem) → CardinalAt.read zero (up b ∷ κ ∷ []) sat , mem }))

upSelf : up self ≡ θ
upSelf = Σ≡Prop (λ x → (isL x) .snd) self-eq

nonempty : ∥ Σ[ b ∶ A ] ⟨ Good b ⟩ ∥₁
nonempty = ∣ self
          , subst (λ z → IsCardinalL z × ⟨ κ .fst ∈ˢ z .fst ⟩)
              (sym upSelf) (cθ , κ∈θ) ∣₁

least : Σ[ b ∶ A ] IsLeast w Good b
least = leastOfFormula w definedGood lem nonempty

δ : SL.S
δ = up (least .fst)

δ∈sθ : ⟨ δ .fst ∈ˢ sucV (θ .fst) ⟩
δ∈sθ = member (sucV (θ .fst)) (least .fst)

oδ : IsOrd (δ .fst)
oδ = mem-ord {A = sucV (θ .fst)} (suc-ord oθ) (δ .fst) δ∈sθ

cδ : IsCardinalL δ
cδ = ((least .snd) .fst) .fst

κ∈δ : ⟨ κ .fst ∈ˢ δ .fst ⟩
κ∈δ = ((least .snd) .fst) .snd

δ-min : (b : A) → ⟨ Good b ⟩ → let module W = SWO w in (b W.<∙ least .fst → ⊥₀)
δ-min = (least .snd) .snd

leastness : (c : SL.S) → IsOrd (c .fst) → IsCardinalL c
          → ⟨ κ .fst ∈ˢ c .fst ⟩
          → (x : SL.S) → ⟨ x .fst ∈ˢ δ .fst ⟩ → ⟨ x .fst ∈ˢ c .fst ⟩
leastness c oc cc κ∈c = go (ord-tri (δ .fst) oδ (c .fst) oc)
  where

  go : Tri (δ .fst) (c .fst)
     → (x : SL.S) → ⟨ x .fst ∈ˢ δ .fst ⟩ → ⟨ x .fst ∈ˢ c .fst ⟩
  go (inl δ∈c)       x x∈δ = oc .fst x∈δ δ∈c
  go (inr (inl e))   x x∈δ = subst (λ v → ⟨ x .fst ∈ˢ v ⟩) e x∈δ
  go (inr (inr c∈δ)) x x∈δ = ⊥₀-rec (δ-min b bGood b<δ)

    where
    c∈sθ : ⟨ c .fst ∈ˢ sucV (θ .fst) ⟩
    c∈sθ = suc-ord oθ .fst c∈δ δ∈sθ
    b : A
    b = fiber (sucV (θ .fst)) c∈sθ .fst

    be : ⟪ sucV (θ .fst) ⟫↪ b ≡ c .fst
    be = fiber (sucV (θ .fst)) c∈sθ .snd
    upb : up b ≡ c
    upb = Σ≡Prop (λ v → (isL v) .snd) be
    bGood : ⟨ Good b ⟩

    bGood = subst (λ z → IsCardinalL z × ⟨ κ .fst ∈ˢ z .fst ⟩)
              (sym upb) (cc , κ∈c)
    b<δ : let module W = SWO w in b W.<∙ least .fst
    b<δ = transport (λ i → sym (w-lt b (least .fst)) i)
            (subst (λ v → ⟨ v ∈ˢ δ .fst ⟩) (sym be) c∈δ)

CardAboveL が与えるのは、κ ∈ θ を満たす何らかの内部順序数基数 θ の命題的に切り詰められた存在だけである。最小性は与えず、θ も選ばない。証明は各局所的な証人を Reduce へ写し、そこで sucV (θ .fst) の提示の内部における最小化を行う。したがって、得られる後続基数も命題的切り詰めの内側に留まる。

succCardExists : SuccCardExists
succCardExists κ oκ cκ κ∉ω = map₁ build (CardAboveL κ oκ cκ κ∉ω)
  where
  build : Σ[ θ ∶ SL.S ]
            (IsOrd (θ .fst) × IsCardinalL θ × ⟨ κ .fst ∈ˢ θ .fst ⟩)

一つの局所的な枝の内部で、build は選ばれた δ を SuccCardL δ κ の四条件と組にする。すなわち、δ は順序数であり、内部基数であり、κ ∈ δ を満たし、さらに κ より大きい任意の内部順序数基数に包含される。

        → Σ[ δ ∶ SL.S ] SuccCardL δ κ
  build (θ , oθ , cθ , κ∈θ) = R.δ , R.oδ , R.cδ , R.κ∈δ , R.leastness
    where module R = Reduce κ oκ θ oθ cθ κ∈θ

構造に関する評価を満たす

指数が順序数である段階は、構成可能である。段階と構成可能性を結ぶ公理によるものである。

stage-is-L : (δ : SL.S) → IsOrd (δ .fst) → ⟨ isL (Lset (δ .fst)) ⟩
stage-is-L δ ordδ = isL-Lset (δ .fst) ordδ

冪集合のための橋渡しの述語は、その内容を述べる。構成可能な集合 κ と y、すなわち κ が順序数であり y がモデルの冪集合 𝒫κ の要素であるとき、y の周囲のすべての要素 z は構成可能であり、κ に属し、順序数でもあるのである。

zStrongest : ModelL.isZFModel → Type (ℓ-suc ℓ)
zStrongest zf =
    (κ y : SL.S) → IsOrd (κ .fst) → ⟨ y .fst ∈ˢ (𝒫 κ) .fst ⟩
  → (z : SV.S) → ⟨ z ∈ˢ y .fst ⟩
  → (⟨ isL z ⟩ × ⟨ z ∈ˢ κ .fst ⟩ × IsOrd z)

この橋渡しは、与えられた ZF モデルに依存する。その前提が、そのモデルによって指定された冪集合を参照するからである。したがって、議論を通じて 𝒫κ は常に L の内部冪集合である。

  where open ModelL.isZFModel zf using ( 𝒫 )

ここで注意すべき点は、量化領域が変わることである。冪集合への所属から得る部分集合の主張は構成可能な集合にわたって量化するが、z は最初、周囲の階層全体を動く。まず L の推移性によって z が構成可能であることを示して初めて、内部の部分集合の主張を適用できる。その後、z ∈ κ と κ の順序数性から z の順序数性が従う。

z-strongest : (zf : ModelL.isZFModel) → zStrongest zf
z-strongest zf κ y ordκ y∈𝒫κ z z∈y = isLz , z∈κ , mem-ord {A = κ .fst} ordκ z z∈κ
  where
  open ModelL.isZFModel zf using ( 𝒫; hasPower )

z の構成可能性は、推移性によって従う。z は構成可能な集合 y に属し、y 自身が構成可能だからである。

  isLz : ⟨ isL z ⟩
  isLz = isL-trans z∈y (y .snd)

モデルの冪集合の定義仕様は、y ∈ 𝒫κ を内部の部分集合関係 y ⊆ κ と同一視する。この関係は SL の要素にわたって量化するので、前の段階で示した構成可能性が不可欠である。

  y⊆κ : ⟨ y ModelL.⊆ˢ κ ⟩
  y⊆κ = subst ⟨_⟩ (ModelL.℩-spec (hasPower κ) y) y∈𝒫κ

内部の部分集合の関係は、z とその構成可能性の対に適用され、z の κ への所属を与える。

  z∈κ : ⟨ z ∈ˢ κ .fst ⟩
  z∈κ = y⊆κ (z , isLz) z∈y

各部分集合は後続基数までに現れる

着地の補題は、モデル・有界部分集合のインターフェース・そして κ の固定された後続基数 δ に対して述べられる。モデルの冪集合 𝒫κ のすべての要素は、段階 Lset δ の中にある。

stage-landing :
    (zf : ModelL.isZFModel) → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → (δ : SL.S) → SuccCardL δ κ
  → (y : SL.S) → ⟨ y .fst ∈ˢ (ModelL.isZFModel.𝒫 zf κ) .fst ⟩

固定した各 y に対して、有界部分集合定理が適切な段階の添字 β を返すのは命題的切り詰めの内側だけである。目標である y ∈ Lset δ 自体が命題なので、すべての y に対して添字を一様に選ぶことなく、局所的な β を用いて議論できる。この定理が要求する周囲の点ごとの部分集合の仮定は、直前に確立した橋渡しそのものである。

  → ⟨ y .fst ∈ˢ Lset (δ .fst) ⟩
stage-landing zf ibs κ ordκ cardκ κ∉ω δ (ordδ , cardδ , κ∈δ , _) y y∈𝒫κ =
  rec₁ ((y .fst ∈ˢ Lset (δ .fst)) .snd) place (ibs κ ordκ cardκ κ∉ω y y⊆κ)
  where
  y⊆κ : (z : SV.S) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ κ .fst ⟩

y ∈ 𝒫κ と z ∈ y から、最強要素補題は z ∈ κ を与える。その証明では、まず L の推移性によって外側の要素 z が構成可能であると分かるので、冪集合への所属が表す内部の部分集合関係を z に適用できる。

  y⊆κ z z∈y = z-strongest zf κ y ordκ y∈𝒫κ z z∈y .snd .fst

δ から κ への単射は存在し得ない。δ は内部の基数であり、κ は δ の要素だからである。この反駁が、下で不可能な三択の分岐を排除する道具である。

  no-δ↪κ : InjL δ κ → ⊥₀
  no-δ↪κ = cardδ κ κ∈δ

固定した部分集合 y に対し、有界部分集合の評価は命題的切り詰めのもとで、y ∈ Lset β を満たし、内部の符号化された単射 β ↪ κ をもつ順序数 β を与える。その証人を局所的に取り出すと、place は順序数の三分法によって β と δ を比較し、y がすでに Lset δ に属することを示す。

  place : Σ[ β ∶ SL.S ]
            (IsOrd (β .fst) × ⟨ y .fst ∈ˢ Lset (β .fst) ⟩ × InjL β κ)
        → ⟨ y .fst ∈ˢ Lset (δ .fst) ⟩
  place (β , ordβ , y∈Lβ , β↪κ) = go (ord-tri (β .fst) ordβ (δ .fst) ordδ)
    where

β が δ より下なら、塔の単調性が、低い段階の要素を高い段階の中に直接置く。β が δ に等しいなら、注入 β ↪ κ は δ ↪ κ になり、δ の基数性と矛盾する。

    go : Tri (β .fst) (δ .fst) → ⟨ y .fst ∈ˢ Lset (δ .fst) ⟩
    go (inl β∈δ)       = Lset-mono β∈δ y∈Lβ
    go (inr (inl e))   = ⊥₀-rec (no-δ↪κ (subst (λ b → InjL b κ) β≡δ β↪κ))
      where
      β≡δ : β ≡ δ

等しい場合には、構成可能性が命題値なので、基礎となる集合の等しさを対応する L の要素の等しさへ持ち上げられる。残る δ ∈ β の場合には、包含から得る δ ↪ β に、与えられた符号化された単射 β ↪ κ を続けると、存在し得ない符号化された単射 δ ↪ κ が生じる。

      β≡δ = Σ≡Prop (λ x → (isL x) .snd) e
    go (inr (inr δ∈β)) = ⊥₀-rec (no-δ↪κ
      (injl-trans δ β κ (inclusion-coded δ β δ⊆β) β↪κ))
      where
      δ⊆β : (z : SV.S) → ⟨ z ∈ˢ δ .fst ⟩ → ⟨ z ∈ˢ β .fst ⟩

包含は、順序数 β の推移性を、二つの所属に適用したものである。

      δ⊆β z z∈δ = ordβ .fst z∈δ δ∈β

冪集合を後続基数の下へコード化する

冪集合の比較は、鎖 𝒫κ ↪ Lset δ ↪ δ から従う。第一の矢印は、内部冪集合のすべての要素が Lset δ に属することから得られ、第二の矢印は、その構成可能な段階を δ で数える。𝒫κ の各要素に対して段階の添字を一様に選ぶことはない。

power-into-succ :
    (zf : ModelL.isZFModel) → StageCountedCoded → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → (δ : SL.S) → SuccCardL δ κ
  → InjL (ModelL.isZFModel.𝒫 zf κ) δ

点ごとの包含は、まず inclusion-coded によって符号化された単射 𝒫κ ↪ Lset δ に変換される。段階計数の仮定が Lset δ ↪ δ を与え、injl-trans が両者を合成する。どちらの比較も InjL で表されるため、それらを証すグラフは命題的切り詰めの内側に留まる。

power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc@(ordδ , _ , κ∈δ , _) =
  injl-trans (𝒫 κ) Lδ δ (inclusion-coded (𝒫 κ) Lδ into)
    (scc δ Lδ ordδ δ∉ω refl)
  where
  open ModelL.isZFModel zf using ( 𝒫 )

δ での段階は、段階の集合とその構成可能性の証明を対にすることで、L の要素として提示される。証明は、δ の順序数性から得られる。

  Lδ : SL.S
  Lδ = Lset (δ .fst) , stage-is-L δ ordδ

後続基数 δ は ω の外にある。もし ω の中にあるなら、所属 κ ∈ δ が ω の推移性によって κ ∈ ω を強制し、仮定と矛盾する。

  δ∉ω : ⟨ δ .fst ∈ˢ ω ⟩ → ⊥₀
  δ∉ω δ∈ω = κ∉ω (ω-ord .fst {x = δ .fst} {y = κ .fst} κ∈δ δ∈ω)

冪集合のすべての要素は、着地の補題によって Lset δ の中に落ちる。その構成可能性は、冪集合への所属から、L の推移性を通して供給される。

  into : (z : SV.S) → ⟨ z ∈ˢ (𝒫 κ) .fst ⟩ → ⟨ z ∈ˢ Lδ .fst ⟩
  into z z∈ =
    stage-landing zf ibs κ ordκ cardκ κ∉ω δ sc (z , isL-trans z∈ ((𝒫 κ) .snd)) z∈

一般連続体仮説

最後の定理では、二つの向きの役割を明確に分ける。段階計数と有界部分集合定理が 𝒫κ ↪ δ を確立する。この単射を得た後で初めて、独立した条件付き定理 SuccIntoPower を適用し、それと後続基数の事実を用いて δ ↪ 𝒫κ を確立する。

gch-from-internal-bill :
    (zf : ModelL.isZFModel)
  → StageCountedCoded → InternalBoundedSubset → SuccIntoPower zf
  → GCHStatement zf
gch-from-internal-bill zf scc ibs sip κ ordκ cardκ κ∉ω =

定理 succCardExists が与えるのは、後続基数 δ の命題的切り詰めのもとでの存在だけである。そこで写像は各局所的な証人の内部で働く。step は後続基数の証明を保ち、着地の議論から命題的切り詰めのもとで符号化された単射 𝒫κ ↪ δ を構成し、その結果を独立した条件付きインターフェースに渡して、同じく切り詰められた符号化された単射 δ ↪ 𝒫κ を得る。

  map₁ step (succCardExists κ ordκ cardκ κ∉ω)
  where
  open ModelL.isZFModel zf using ( 𝒫 )
  step : Σ[ δ ∶ SL.S ] SuccCardL δ κ
       → Σ[ δ ∶ SL.S ] (SuccCardL δ κ × InjL (𝒫 κ) δ × InjL δ (𝒫 κ))

着地の議論は pis : InjL (𝒫 κ) δ を与え、独立した条件付きインターフェースは pis を前提として InjL δ (𝒫 κ) を与える。各 InjL は、構成可能な単射の符号が存在することの命題的切り詰めである。したがって結果が記録するのは、ちょうど反対向きの二つの符号化された単射の存在であり、どちらのグラフも選択せず、全単射、集合の等しさ、基数算術上の等式も構成しない。

  step (δ , sc) = δ , sc , pis , sip κ δ κ∉ω sc pis
    where
    pis : InjL (𝒫 κ) δ
    pis = power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc