後続基数を冪集合へ単射する

対角線論法を通して、𝒫 κ は固定した L 上の ZF モデルが与える冪集合を意味する。したがって、その要素は、まさにこのモデルの内部で認識される部分集合である。

open ModelL.isZFModel zf using ( 𝒫 )

対角の議論は、明示的に与えられた一つのグラフ F とその符号について展開される。後の主張はすべて、この固定されたグラフに関するものである。

module Diag (F : SL.S) (code : InjCode F (𝒫 κ) κ) where

γF : Vec SL.S 
γF = F ∷ 𝒫 κ ∷ []

ranF : (x y : SL.S) → Holds F x y → ⟨ y .fst ∈ κ .fst ⟩
ranF = code .snd .snd .snd

valF : (x : SL.S) → ⟨ x .fst ∈ (𝒫 κ) .fst ⟩
     → ∥ Σ[ y ∶ SL.S ] Holds F x y ∥₁
valF = domAt-in zero (suc zero) γF (code .snd .fst)

injF : (y x x' : SL.S) → Holds F x y → Holds F x' y → x .fst ≡ x' .fst
injF = injAt-out zero γF (code .snd .snd .fst)

Diagonal : SL.S → Type (ℓ-suc ℓ)
Diagonal ξ = ∥ Σ[ A ∶ SL.S ] ( ⟨ A .fst ∈ (𝒫 κ) .fst ⟩ × Holds F A ξ
                             × (⟨ ξ .fst ∈ A .fst ⟩ → ⊥₀) ) ∥₁

private
  a1 : (ξ A : SL.S)
     → ⟨ (A ∷ ξ ∷ []) ⊨ appC F zero (suc zero) ⟩ ≡ Holds F A ξ
  a1 ξ A = cong ⟨_⟩ (appC-adequate F zero (suc zero) (A ∷ ξ ∷ []))

opaque
  φD : Formula SL.S 
  φD = ∃̇∈ (con (𝒫 κ))
         (appC F zero (suc zero) ∧̇ ¬̇ (var (suc zero) ∈̇ var zero))

  φD-out : (ξ : SL.S) → ⟨ (ξ ∷ []) ⊨ φD ⟩ → Diagonal ξ
  φD-out ξ = map₁ (λ { (A , (mA , (h , n))) →
    A , mA , transport (a1 ξ A) h , (λ k → lower (n k)) })

  φD-in : (ξ A : SL.S) → ⟨ A .fst ∈ (𝒫 κ) .fst ⟩ → Holds F A ξ
        → (⟨ ξ .fst ∈ A .fst ⟩ → ⊥₀) → ⟨ (ξ ∷ []) ⊨ φD ⟩
  φD-in ξ A mA h n =
    ∣ A , (mA , (transport (sym (a1 ξ A)) h , (λ k → lift (n k)))) ∣₁

D₀ : SL.S
D₀ = ((hasSeparationL κ φD) .fst) .fst

D₀-spec : (ξ : SL.S) → (ξ SL.∈ˢ D₀) ≡ ((ξ SL.∈ˢ κ) ⊓ ((ξ ∷ []) ⊨ φD))
D₀-spec = ((hasSeparationL κ φD) .fst) .snd

D₀∈𝒫κ : ⟨ D₀ .fst ∈ (𝒫 κ) .fst ⟩
D₀∈𝒫κ = into-power zf κ D₀ (λ z h → (subst ⟨_⟩ (D₀-spec z) h) .fst)

absurd : Σ[ ξ ∶ SL.S ] Holds F D₀ ξ → ⊥₀
absurd (ξ , h₀) = out inside
  where

  out : ⟨ ξ .fst ∈ D₀ .fst ⟩ → ⊥₀
  out hm = rec₁ isProp⊥
    (λ { (A , _ , hA , n) →
      n (subst (λ w → ⟨ ξ .fst ∈ w ⟩) (injF ξ D₀ A h₀ hA) hm) })
    (φD-out ξ ((subst ⟨_⟩ (D₀-spec ξ) hm) .snd))

  inside : ⟨ ξ .fst ∈ D₀ .fst ⟩
  inside = subst ⟨_⟩ (sym (D₀-spec ξ))
    (ranF D₀ ξ h₀ , φD-in ξ D₀ D₀∈𝒫κ h₀ out)

この二つの半分が、冪集合から κ への内部の符号化された単射をすべて反証する。単射はグラフへ消去され、グラフの対角の集合における値が矛盾へ消去される。目標が空の型なので、どちらの消去も正当である。

no-inj : InjL (𝒫 κ) κ → ⊥₀
no-inj = rec₁ isProp⊥ step
  where
  step : Σ[ F ∶ SL.S ] InjCode F (𝒫 κ) κ → ⊥₀
  step (F , code) = rec₁ isProp⊥ D.absurd (D.valF D.D₀ D.D₀∈𝒫κ)

選んだグラフ F に対して、対角構成は内部部分集合 D₀ と、そこに値を割り当てることが不可能であるという証明を与える。それでも全域性は値を割り当てるので、このグラフについて矛盾が完成する。

    where module D = Diag F code

ここで始域となる 𝒫 κ も、固定した ZF モデルが定める内部の冪集合である。この構成で、それを底の集合の周囲の冪集合に置き換えることはない。

open ModelL.isZFModel zf using ( 𝒫 )

後続の順序数性は、その記録の最初の成分である。

ordδ : IsOrd (δ .fst)
ordδ = sc .fst

冪集合が、比較の源として名付けられる。

P : SL.S
P = 𝒫 κ

グラフの環境は、グラフと冪集合を対にする。

γG : Vec SL.S 
γG = G ∷ P ∷ []

符号の値域の条項は、すべての値が後続の中に着地することを言う。

ranG : (x y : SL.S) → Holds G x y → ⟨ y .fst ∈ δ .fst ⟩
ranG = code .snd .snd .snd

一価性は一つの固定した入力についての性質である。G が G(x)=y と G(x)=y' の両方を記録するなら、y と y' の底の集合は等しくなる。この一意性により、x の可能な値からなる型が命題になる。

svG : (x y y' : SL.S) → Holds G x y → Holds G x y' → y .fst ≡ y' .fst
svG = svAt-out zero γG (code .fst)

全域性は、各 x ∈ P に対して命題的に切り詰められた値の証人を与える。この時点では、値はまだ選ばれていない。すぐ後で一価性から可能な値のファイバーが命題であることを示し、この切り詰めから消去して局所的に値を読み出す。

valG : (x : SL.S) → ⟨ x .fst ∈ P .fst ⟩ → ∥ Σ[ y ∶ SL.S ] Holds G x y ∥₁
valG = domAt-in zero (suc zero) γG (code .snd .fst)

符号化された単射 G の単射性の条項は、値から始域の要素を復元する。二つの始域の要素が同じ記録値をもつなら、それらの底の集合は等しくなる。

injG : (y x x' : SL.S) → Holds G x y → Holds G x' y → x .fst ≡ x' .fst
injG = injAt-out zero γG (code .snd .snd .fst)

入力 x を固定すると、G のグラフが与える任意の二つの値は、一価性によって等しくなる。構成可能性の証明は命題なので、基礎にある値の等しさは証人全体の等しさへ持ち上がる。したがって、可能な値からなるファイバー自身が命題である。

isPropVal : (x : SL.S) → isProp (Σ[ y ∶ SL.S ] Holds G x y)
isPropVal x (y , h) (y' , h') =
  Σ≡Prop (λ w → (pr (x .fst) (w .fst) ∈ G .fst) .snd) (S≡ (svG x y y' h h'))

定義域の条項が最初に与える G の値は、命題的切り詰めの内側にある。直前に示した一意性によって行き先のファイバーは命題値になるので、切り詰めを除去し、その一意な値を以後の構成で使える。この段階で用いるのは一意性であり、一般の選択原理ではない。

val : (x : SL.S) → ⟨ x .fst ∈ P .fst ⟩ → Σ[ y ∶ SL.S ] Holds G x y
val x m = rec₁ (isPropVal x) (λ z → z) (valG x m)

a が b に先行するとは、両者が P に属し、G(a)=x、G(b)=y、x∈y を満たすグラフの値 x と y が命題的切り詰めのもとで存在することだと定める。命題的切り詰めは、適切な像が存在することだけを記録し、証人の選択は保持しない。

Read : SL.S → SL.S → Type (ℓ-suc ℓ)
Read a b = ∥ Σ[ x ∶ SL.S ] Σ[ y ∶ SL.S ]
             ( ⟨ a .fst ∈ P .fst ⟩ × ⟨ b .fst ∈ P .fst ⟩
             × Holds G a x × Holds G b y × ⟨ x .fst ∈ y .fst ⟩ ) ∥₁

この関係を対象言語で表すため、環境は A、B と、その像の候補 x、y を、G の二つの適用から読める位置に置く。これにより、一つの論理式で G(A)=x、G(B)=y、x∈y を同時に述べられる。

private
  env5 : SL.S → SL.S → SL.S → SL.S → SL.S → Vec SL.S 
  env5 p A B x y = y ∷ x ∷ B ∷ A ∷ p ∷ []

最初の妥当性の等式は、符号化された適用をグラフの主張 Holds G A x と同一視する。これは、対象言語の論理式と、符号化されたグラフが A を x へ送るという主張を結ぶ橋である。

  b1 : (p A B x y : SL.S)
     → ⟨ env5 p A B x y ⊨ appC G (suc (suc (suc zero))) (suc zero) ⟩
     ≡ Holds G A x
  b1 p A B x y = cong ⟨_⟩
    (appC-adequate G (suc (suc (suc zero))) (suc zero) (env5 p A B x y))

二つ目の妥当性の等式は、B と y について同じ変換を行う。二つの等式を合わせることで、引き戻した関係を、論理式の充足からも、G のグラフについての通常の主張からも証明できる。

  b2 : (p A B x y : SL.S)
     → ⟨ env5 p A B x y ⊨ appC G (suc (suc zero)) zero ⟩ ≡ Holds G B y
  b2 p A B x y = cong ⟨_⟩
    (appC-adequate G (suc (suc zero)) zero (env5 p A B x y))

定義する論理式は、まず二つの端点を内部冪集合に制限し、続いてそれらの像となる二つのモデル要素を量化する。二つの適用のアトムと、像の間の所属比較を合わせることで、P 上の関係の一階的な記述が得られ、関係の構成はその記述を L の集合として表す。

private
  opaque
    φR : Formula SL.S 
    φR = (var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ∃̇ (∃̇
      (appC G (suc (suc (suc zero))) (suc zero)

二つの存在束縛の内側で、残りの条項は、二つの証人がそれぞれ端点の G による像であり、最初の像が二つ目の像に属することを述べる。これはまさに、δ 上の所属順序を G に沿って引き戻したものである。

        ∧̇ (appC G (suc (suc zero)) zero ∧̇ (var (suc zero) ∈̇ var zero)))))

論理式を外向きに読むと、まず二つの像の証人が命題的切り詰めのもとに保たれる。次に、二つの妥当性の等式が符号化された適用をグラフの事実へ変え、Read の意味論的データ、すなわち端点の所属、二つの値、その間の所属比較をちょうど与える。

    read : (a b p : SL.S) → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ → Read a b
    read a b p (ma , mb , h) = rec₁ squash₁
      (λ { (x , hx) → map₁ (λ { (y , ha , hb , hxy) → x , y , ma , mb
        , transport (b1 p a b x y) ha , transport (b2 p a b x y) hb , hxy }) hx }) h

内向きの読み出しは、逆向きの妥当性の等式に沿って、それぞれのホスト側の事実を運び戻し、存在量化子と適用の枠を満たして、論理式の充足を再構築する。

    fill : (a b p : SL.S) → Read a b → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩
    fill a b p = rec₁ (((b ∷ a ∷ p ∷ []) ⊨ φR) .snd)
      (λ { (x , y , ma , mb , ha , hb , hxy) → ma , mb , ∣ x , ∣ y
        , transport (sym (b1 p a b x y)) ha
        , transport (sym (b2 p a b x y)) hb , hxy ∣₁ ∣₁ })

有界関係の構成は、この定義可能な述語を L にある実際の関係集合へ変える。上で示した二方向の読み替えにより、符号化された関係への所属は、Read が表す命題的に切り詰められた内容とちょうど一致する。

  module Pullback = Relation P P φR (λ a b → Read a b , squash₁) read fill

逆向きに読むときは、二つの妥当性の等式によって、グラフの事実 Holds G A x と Holds G B y を適用のアトムへ戻す。続いて x と y を二つの存在量化の証人としてまとめると、定義論理式の充足が再構成される。

R : SL.S
R = Pullback.rel

R の一つの関係項から、引き戻しを定義する命題的に切り詰められたデータを読み戻せる。すなわち、二つの端点は冪集合に属し、それぞれ G による像をもち、最初の像は二つ目の像に属する。

R-out : (a b : SL.S) → Holds R a b → Read a b
R-out = Pullback.pair-out

内向きの読み出しは、二つの端点の所属、G の像の二つの事実、そして像の間の所属から、関係の項目を作る。

R-in : (a b x y : SL.S) → ⟨ a .fst ∈ P .fst ⟩ → ⟨ b .fst ∈ P .fst ⟩
     → Holds G a x → Holds G b y → ⟨ x .fst ∈ y .fst ⟩ → Holds R a b
R-in a b x y ma mb ha hb hxy = Pullback.into a b ma mb ∣ x , y , ma , mb , ha , hb , hxy ∣₁

符号化された関係の各項目では、二つの端点がとも P に属する。証明は命題的切り詰めのもとにある証人を読み、像のデータを捨てて、二つの端点の所属だけを残す。その積は命題なので、この切り詰めの除去が許される。

Rsub : (a b : SL.S) → Holds R a b
     → ⟨ a .fst ∈ P .fst ⟩ × ⟨ b .fst ∈ P .fst ⟩
Rsub a b h = rec₁
  (isProp× ((a .fst ∈ P .fst) .snd) ((b .fst ∈ P .fst) .snd))
  (λ { (_ , _ , ma , mb , _) → ma , mb })

外向きの読み出しを適用すると、抽出に必要な証人が得られる。その切り詰めを除去できるのは、結論である二つの端点の所属命題の組もまた命題だからである。

  (R-out a b h)

順序型の構成は、P の要素を小さい提示領域 Dom で表す。関係 a ≺ b は、表された要素どうしが R で関係づけられるという符号化された事実をちょうど記録する。そこで以下では、添字上の引き戻し順序を調べ、のちにそれを崩壊できる。

module OT = Code P R Rsub
  using ( Dom; Dom≡; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out
        ; module Conjuncts )

この領域の添字 b に対し、v b を、b が表す P の要素へ G が割り当てる一意な値とする。次に、これらの代表が δ より下の順序数であることを示す。

v : OT.Dom → SL.S
v b = (val (OT.up b) (OT.up-mem b)) .fst

選んだ値の第二成分は、対応するグラフの事実 Holds G (up b) (v b) を記録する。これは、代表どうしの比較を引き戻した関係の項目へ結びつける。

v-holds : (b : OT.Dom) → Holds G (OT.up b) (v b)
v-holds b = (val (OT.up b) (OT.up-mem b)) .snd

単射の符号の値域の条項により、G の各値は後続基数 δ に属する。したがって、すべての代表が一つの順序数の中にあり、そこで所属による比較と順序数の三分法を用いられる。

v∈δ : (b : OT.Dom) → ⟨ (v b) .fst ∈ δ .fst ⟩
v∈δ b = ranG (OT.up b) (v b) (v-holds b)

それぞれの G の値は順序数である。δ の順序数性から受け継がれる。

ord-v : (b : OT.Dom) → IsOrd ((v b) .fst)
ord-v b = mem-ord {A = δ .fst} ordδ ((v b) .fst) (v∈δ b)

前向きの比較は、引き戻された関係の一つの先行段階を、二つの代表順序数の間の所属へ移す。関係の項目を読むと二つの像の証人が得られ、G の一価性によって、それぞれが固定した値 v a と v b に同一視される。

≺-fwd : (a b : OT.Dom) → a OT.≺ b → ⟨ (v a) .fst ∈ (v b) .fst ⟩
≺-fwd a b k = rec₁ (((v a) .fst ∈ (v b) .fst) .snd)
  (λ { (x , y , _ , _ , ha , hb , hxy) →
    subst2 (λ s t → ⟨ s ∈ t ⟩)
      (svG (OT.up a) x (v a) ha (v-holds a))

二つの一価性の等式により、R から読み出した像の証人を、固定した代表 v a と v b にそれぞれ置き換える。x∈y を両方の等式に沿って輸送すると、必要な比較 v a ∈ v b が得られる。

      (svG (OT.up b) y (v b) hb (v-holds b)) hxy })
  (R-out (OT.up a) (OT.up b) (OT.≺-out a b k))

後ろ向きの比較は、二つの代表の順序数の所属から、引き戻された関係を構成する。二つのグラフの事実と、像の間の所属を、改めて導入することによるものである。

≺-bwd : (a b : OT.Dom) → ⟨ (v a) .fst ∈ (v b) .fst ⟩ → a OT.≺ b
≺-bwd a b h = OT.≺-in a b
  (R-in (OT.up a) (OT.up b) (v a) (v b)
    (OT.up-mem a) (OT.up-mem b) (v-holds a) (v-holds b) h)

整礎性を示すため、階層の要素 u を固定し、代表の値が u であるすべての領域の添字を考える。述語 Pacc u は、その各添字が引き戻し順序でアクセス可能であることを要求し、周囲の所属関係に関する帰納を準備する。

private
  Pacc : V ℓ → Type (ℓ-suc ℓ)
  Pacc u = (b : OT.Dom) → (v b) .fst ≡ u → Acc OT._≺_ b

帰納のステップは、代表の順序数が u より厳密に下にある先行者のアクセス可能性を構成する。前向きの比較が所属を代表へ運び、帰納の仮定がそこでアクセス可能性を供給する。

  accStep : (u : V ℓ) → (∀ u' → ⟨ u' ∈ˢ u ⟩ → Pacc u') → Pacc u
  accStep u IH b e = acc (λ a k →
    IH ((v a) .fst) (subst (λ w → ⟨ (v a) .fst ∈ˢ w ⟩) e (≺-fwd a b k))
       a refl)

すべての階層の要素でのアクセス可能性は、周囲の階層の正則性の帰納で証明される。それは、所属の整礎性である。

  accAt : (u : V ℓ) → Pacc u
  accAt = WF.WFI.induction regularityV {P = Pacc} accStep

引き戻された順序の整礎性は、代表の順序数ごとのアクセス可能性から組み立てられる。

wf : WellFounded OT._≺_
wf b = accAt ((v b) .fst) b refl

引き戻された順序の推移性は、二つの前向きの比較を、順序数 δ の推移性を二つの代表の所属に適用して合成する。

≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
≺-trans {a} {b} {c} k k' = ≺-bwd a c
  (ordδ .snd ((v c) .fst) (v∈δ c) (≺-fwd a b k) (≺-fwd b c k'))

引き戻された順序の三分法は、δ にある代表値についての順序数の三分法から移される。任意の a と b に対して、v a ∈ v b、二つの値が等しい、v b ∈ v a のいずれかが成り立つ。

tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
tri a b = go (ord-tri ((v a) .fst) (ord-v a) ((v b) .fst) (ord-v b))
  where
  go : Tri ((v a) .fst) ((v b) .fst)
     → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))

厳密に下の場合は、引き戻された比較を直接作る。等しい場合は、等しい代表の値に G の単射性を適用して、二つの定義域の要素を同一視する。厳密に上の場合は比較を逆向きにする。

  go (inl h)       = inl (≺-bwd a b h)
  go (inr (inl e)) = inr (inl (OT.Dom≡
    (injG (v a) (OT.up a) (OT.up b) (v-holds a)
      (subst (λ w → ⟨ pr (OT.↪ b) w ∈ G .fst ⟩) (sym e) (v-holds b)))))
  go (inr (inr h)) = inr (inr (≺-bwd b a h))

整礎性と推移性から、崩壊写像 col とその像 otL が得られる。三分法を加えると崩壊の単射性も従い、異なる領域の添字が同じ崩壊値をもつことはない。これらの事実は、崩壊の表と、あとでそれを逆向きに読むためのデータの両方を与える。

module C = OT.Conjuncts wf ≺-trans
  using ( module Inj; col; col-ord; col-out; colTable; colTable-in
        ; colTable-pair; otL; otL-in; otL-out )
module I = C.Inj tri using ( code; col-inj; module Inverse )

崩壊の表は、内部の冪集合 P からその崩壊像 otL への符号化された単射である。その特定の表と単射性の証明を命題的に切り詰めることで、内部の主張 InjL P otL が得られる。

power-into-ot : InjL P C.otL
power-into-ot = ∣ C.colTable , I.code ∣₁

崩壊像が順序数であることを示すには、像自身の推移性と、その各要素が推移的集合であることの両方が必要である。後者について、otL への所属から、命題的切り詰めのもとで、与えられた要素を崩壊値として提示する添字 b が得られる。

ot-ord : IsOrd (C.otL .fst)
ot-ord = tr , mem
  where
  mem : (x : V ℓ) → ⟨ x ∈ˢ C.otL .fst ⟩ → isTransV x
  mem x h = rec₁ (isPropIsTransV x)

各崩壊値 col b はすでに順序数だと分かっているので、推移的である。この推移性を等式 col b = x に沿って輸送すれば、像の任意の要素 x が推移的であることが従う。

    (λ { (b , e) → subst isTransV e (C.col-ord b .fst) })
    (C.otL-out x h)

残るのは、像自身が推移的であることである。y∈x と x∈otL が与えられると、otL の外向きの記述は、命題的切り詰めのもとで x をある崩壊値 col b として提示する。目標の所属 y∈otL は命題なので、この証人を局所的に使える。

  tr : isTransV (C.otL .fst)
  tr {x} {y} y∈x x∈ot =
    rec₁ ((y ∈ˢ C.otL .fst) .snd) outer (C.otL-out x x∈ot)
    where
    outer : Σ[ b ∶ OT.Dom ] (C.col b ≡ x) → ⟨ y ∈ˢ C.otL .fst ⟩

x を col b に置き換えると、col b への所属を述べる崩壊の等式から、再び命題的切り詰めのもとで、崩壊値が y である先行者 r≺b が得られる。この小さい崩壊値が、y を像へ戻すために必要な証人である。

    outer (b , e) = rec₁ ((y ∈ˢ C.otL .fst) .snd) inner
      (C.col-out b y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym e) y∈x))
      where
      inner : Σ[ r ∶ OT.Dom ] ((r OT.≺ b) × (C.col r ≡ y))
            → ⟨ y ∈ˢ C.otL .fst ⟩

先行者の崩壊がその等式に沿って y へ運ばれ、y を像の中に置くことで、推移性の証明が完成する。

      inner (r , _ , e2) =
        subst (λ w → ⟨ w ∈ˢ C.otL .fst ⟩) e2 (C.otL-in r)

階層の要素 w に対し、ファイバー Fib w は添字 b と等式 col b = w からなる。したがって、このファイバーの要素は、崩壊写像による w の原像そのものである。

Fib : V ℓ → Type (ℓ-suc ℓ)
Fib w = Σ[ b ∶ OT.Dom ] (C.col b ≡ w)

col の単射性により、各ファイバーは命題になる。b と b' がともに w へ崩壊するなら、それらの等式から col b と col b' が等しくなり、単射性によって添字も等しくなる。周囲の階層 V ℓ は集合なので、各等式型 col b = w は命題であり、その証明が新たな違いを生むこともない。

isPropFib : (w : V ℓ) → isProp (Fib w)
isPropFib w (b , e) (b' , e') =
  Σ≡Prop (λ _ → setIsSet _ _) (I.col-inj b b' (e ∙ sym e'))

所属 w∈otL が最初に与える原像の添字は、命題的切り詰めの内側にある。Fib w が命題であることを直前に示したので、この切り詰めを除去し、崩壊値が w である一意な添字を取り出せる。

fib : (w : V ℓ) → ⟨ w ∈ˢ C.otL .fst ⟩ → Fib w
fib w h = rec₁ (isPropFib w) (λ z → z) (C.otL-out w h)

いま得た一意な原像により、崩壊の表を otL 全体で逆向きに読める。その添字が表すもとの要素は P に属するので、逆向きの構成は L にあるグラフを作り、とくに以下で用いる内部の符号化された単射 Back.injL : InjL otL P を与える。

module Back where

open I.Inverse C.otL P (λ w mw → fib (w .fst) mw)
  (λ w mw → OT.up-mem (fib (w .fst) mw .fst)) public
  using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )

崩壊順序数 otL を μ と書く。順序数の三分法によって μ と後続基数 δ を比較する。補助関数 from-sub は、等しい場合と δ∈μ の場合に共通する構成を取り出す。δ のすべての要素が μ にも属するなら、必要な InjL δ P を作る。

result : InjL δ P
result = go (ord-tri (C.otL .fst) ot-ord (δ .fst) ordδ)
  where
  from-sub : ((z : SV.S) → ⟨ z ∈ˢ δ .fst ⟩ → ⟨ z ∈ˢ C.otL .fst ⟩)
           → InjL δ P

包含の符号が、部分集合の事実を、δ から崩壊の像への符号化された単射としてまとめ、逆崩壊の単射がそれを冪集合の中へ合成する。

  from-sub sub =
    injl-trans δ C.otL P (inclusion-coded δ C.otL sub) Back.injL

三分法では、まず μ∈δ の場合を考える。この場合、below-succ-injects は後続基数の事実を用いて InjL μ κ を与える。これを InjL P μ と合成すると InjL P κ が得られ、内部の Cantor の定理に反する。したがって排除されるのは、崩壊順序数が δ より真に小さい場合だけである。

  go : Tri (C.otL .fst) (δ .fst) → InjL δ P
  go (inl ot∈δ)       = ⊥₀-rec (Cantor.no-inj zf κ
    (injl-trans P C.otL κ power-into-ot
      (below-succ-injects κ δ sc C.otL ot-ord ot∈δ)))
  go (inr (inl e))    =

残る二つの場合は、どちらも from-sub に必要な包含を与える。μ=δ なら、等式に沿う輸送によって、δ への各所属が μ への所属になる。δ∈μ なら、順序数 μ の推移性から同じ包含 δ⊆μ が得られる。いずれの場合も、この包含を単射として符号化し、逆崩壊の単射と合成することで InjL δ P を得る。

    from-sub (λ z h → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) h)
  go (inr (inr δ∈ot)) =
    from-sub (λ z h → ot-ord .fst h δ∈ot)