L の内部における構成可能階層

宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

L 内の一階のグラフは、指定した順序数までの外部の構成可能階層を記録する。表の値を外部の塔と照らして関数的かつ正確であると示し、そののち、これらの対を、それより前の段階をちょうど要素とする構成可能集合へ集める。

本章は内部の階層を構成する。階層の順序数 α に対し、hierL の α での値は L の要素であり、その要素は「α の下の順序数 β と塔の値 Lset β」の順序対ちょうどである。一つのパターンが章全体で繰り返される。表とは順序対の集合であり、集合 B の下で記録する値がすべてメタレベルの塔のそこでの値であるとき、B の上で正しいと言い、その下のすべての入力で値を記録しているとき完備と言う。正しくて完備な表こそ、グラフのステップ条件が読むものであり、そこから書き下せるものでもある。だからステップと塔を結ぶ補題の組が、消去と導入の両方に仕える。

本章は、モデル自身のレベルの後続で排中律の実例を一つ取り、そのもとで進む。以下の構成はすべてこのモジュールの内部で述べられ、公理の章が渡す場所でだけこの仮定を帯ぶ。

ここでは二つの構造が現れる。周囲の階層はその構造 𝒮ᵥ を与え、本章はその所属の帰納と外延性を用いる。構成可能な構造 𝒮ʟ は台 S を与える。その要素は、階層の集合に「それが構成可能である」証明を添えたものであり、だから各台の要素 x には基礎の集合 x .fst がある。

階層は、章を通して使う三つの道具を与える。所属に沿う帰納、集合の外延性、そして順序対 pr と、その成分を取り戻す単射性である。この対は階層のレベルにあり、表の記録された項目も同じレベルにある。

構成可能の側からは、塔 Lset が来る。これは階層の順序数を、そこでの構成可能段階へ送る。ほかに、定義可能冪集合 𝒟ₒ、二つの所属の読み Lset-in と Lset-out、順序数性 IsOrd、そして「構成可能性が所属に沿って伝わる」事実である。塔の添字は順序数、すなわち階層の集合であり、型の大きさの添字である宇宙レベルでは決してない。

さらに三つの事実が章を支える。順序数の要素は順序数であること。段階は L の要素として提示でき、それを LsetS と書き、構成可能集合の定義可能冪集合はまた構成可能であること。そして L の内部では置換が使え、その形は「一意に存在するとだけ分かっている値」を受け入れるものである。

モデルは自分自身の順序対 prʟ と、その第一射影を同定する読み prʟ-fst、そして定義域の条項 domAt-intro を与える。

一つ前の符号化の章は、本章が組み立てる語彙を供給する。証人と三つの読みをもつステップ条件、定義域・値・ステップの条項をもつ近似、二つの読みをもつ塔のグラフ、そして順序対のグラフである。

命題の機構はいつものものである。切り詰められた存在、その注入と消去、第二成分が命題である対が第一成分の等しさで等しくなること、そして所属の各点での同値を集合のパスへ変える操作である。

階層そのものが型として現れる。その要素は本章が表にする集合であり、その所属は三つの条件が語る関係であり、その h-集合性により、表にされた二つの集合の等しさは命題になる。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

構成可能な構造の内側では、S が台であり、⊨ が充足の判断である。SetOf は候補の集合と「それがクラスを実現する」という主張を組にする。record のフィールドが公理を述べるのはこの形である。

open hPropView 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

充足は最後に、構成可能な構造で読まれる。章を通しての記法 γ ⊨ φ は、L から取った定数をもつ論理式を、台の要素の環境で判定する。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

一つの private な補助は、変数の枠を二つ後ろへずらす。値を一つ、次に入力を一つ追加した環境の中でステップを判定するとき、古い枠はみな二つ後ろへ移る。表自身の項目の内側からそのステップを判定する場面で、いつも現れる。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

表が記録するもの

表とは順序対の集合であり、ここではつねに階層の対で取った対、すなわち入力と値の組である。界集合 B の上での表を三つの条件が特徴づける。それらは補い合う条件であって、一つの主張の三つの読みではない。Values は、B の下で記録された値がすべて塔のそこでの値であることを要求する。Entries は、B の下のすべての入力で正準な項目が記録されていることを要求する。Domain は、B の外が何も記録されていないことを要求する。

Values : S → V ℓ → Type (ℓ-suc ℓ)
Values h B = (c z : S) → ⟨ c .fst ∈ B ⟩
           → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩ → z .fst ≡ Lset (c .fst)

正しさは、記録された項目についての主張である。B の下の入力 c とある z の対が表の項目なら、z は塔の c での値である。所属 c .fst ∈ B は階層での所属である。B が階層の集合だからである。表 h は台の要素であり、h .fst がそれが提示する集合である。

Entries : S → V ℓ → Type (ℓ-suc ℓ)
Entries h B = (c : S) → ⟨ c .fst ∈ B ⟩ → ⟨ pr (c .fst) (Lset (c .fst)) ∈ h .fst ⟩

完備さは、覆いについての鏡像の要求である。B の下の各入力 c で、正準な項目、すなわち c と塔の値 Lset c の対が記録される。二つの条件から、正しくて完備な表は B の下で正準な項目ちょうどを記録し、歪んだものを一切含まないことが分かる。

Domain : S → V ℓ → Type (ℓ-suc ℓ)
Domain h B = (c z : S) → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩ → ⟨ c .fst ∈ B ⟩

条件を分けておくのは、応用ごとに必要な部分が異なるからである。近似についての帰納は最初の二つを使い、三つ目は使えない。近似の項目はそれ自身の定義域の下に落ちるのであって、帰納が立っている入力の下ではないからである。内部の階層は三つすべてを満たす。正しい対ちょうどの集合として作られるからである。B が何であるかにも注意してほしい。基礎の界集合、すなわち階層の集合である。意味論的な応用では、環境の枠を通して届き、台の要素の基礎の部分として現れる。その台の要素はさらに構成可能性を帯びており、B の順序数性はこれらの条件が供給しない独立の仮定である。ここで表にされる段階は階層の集合で、順序数で添字づけられる。ホストの宇宙レベルが表に現れることはない。

外部の階層と照らすステップ

この節は、前章のステップ条件と塔を結ぶ。入力 b でのステップは、b の下の入力 c とそこで記録された値 w にわたって、w の定義可能冪集合の要素を集める。塔が b で集める要素は同じもので、記録された w を Lset c に置き換えたものである。三つの private な事実が比較の準備をする。ok は横条件 PowOK を清算し、below は塔の分解をステップの証人に変え、above はステップの証人を塔の要素に変える。

module _ {n : ℕ} (v b f : Fin n) (γ : Vec S n) where

private

  ok : IsOrd ((lookup b γ) .fst) → Values (lookup f γ) ((lookup b γ) .fst)
     → PowOK b f γ

  ok ob vals c z rec = subst (λ u → ⟨ isL (𝒟ₒ u) ⟩)
    (sym (vals c z (rec .fst) (rec .snd)))
    (isL-𝒟ₒ (c .fst) (mem-ord {A = (lookup b γ) .fst} ob (c .fst) (rec .fst)))

  below : IsOrd ((lookup b γ) .fst) → Entries (lookup f γ) ((lookup b γ) .fst)
        → (z : S)
        → Σ[ δ ∶ V ℓ ] (⟨ δ ∈ (lookup b γ) .fst ⟩ × ⟨ z .fst ∈ 𝒟ₒ (Lset δ) ⟩)
        → StepOf b f γ z

  below ob ents z (δ , (δ∈ , hz)) =
    d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz))

    where
    oδ : IsOrd δ
    oδ = mem-ord {A = (lookup b γ) .fst} ob δ δ∈
    d : S
    d = δ , isL-trans {x = (lookup b γ) .fst} {y = δ} δ∈ (lookup b γ .snd)

  above : Values (lookup f γ) ((lookup b γ) .fst) → (z : S) → StepOf b f γ z
        → ⟨ z .fst ∈ Lset ((lookup b γ) .fst) ⟩

  above vals z (c , (w , (rec , hz))) =
    Lset-in ((lookup b γ) .fst) (c .fst) (z .fst) (rec .fst)
      (subst (λ u → ⟨ z .fst ∈ 𝒟ₒ u ⟩) (vals c w (rec .fst) (rec .snd)) hz)

step-Lset : ⟨ γ ⊨ StepAt v b f ⟩ → IsOrd ((lookup b γ) .fst)
          → Values (lookup f γ) ((lookup b γ) .fst)
          → Entries (lookup f γ) ((lookup b γ) .fst)
          → (lookup v γ) .fst ≡ Lset ((lookup b γ) .fst)

step-Lset h ob vals ents =
  extensionalV {a = (lookup v γ) .fst} {b = Lset ((lookup b γ) .fst)} pt
  where

  fwd : (x : V ℓ) → ⟨ x ∈ (lookup v γ) .fst ⟩
      → ⟨ x ∈ Lset ((lookup b γ) .fst) ⟩
  fwd x hx = rec₁ ((x ∈ Lset ((lookup b γ) .fst)) .snd) (above vals z)
    (StepAt-out v b f γ h (ok ob vals) z hx)

    where
    z : S
    z = x , isL-trans {x = (lookup v γ) .fst} {y = x} hx (lookup v γ .snd)

  bwd : (x : V ℓ) → ⟨ x ∈ Lset ((lookup b γ) .fst) ⟩
      → ⟨ x ∈ (lookup v γ) .fst ⟩
  bwd x hx = rec₁ ((x ∈ (lookup v γ) .fst) .snd) put
    (Lset-out ((lookup b γ) .fst) x hx)

    where
    z : S
    z = x , isL-trans {x = Lset ((lookup b γ) .fst)} {y = x} hx
              (LsetS ((lookup b γ) .fst) ob .snd)

    put : Σ[ δ ∶ V ℓ ] (⟨ δ ∈ (lookup b γ) .fst ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
        → ⟨ x ∈ (lookup v γ) .fst ⟩
    put s = StepAt-back v b f γ h (ok ob vals) z (below ob ents z s)

  pt : (x : V ℓ) → (x ∈ (lookup v γ) .fst) ≡ (x ∈ Lset ((lookup b γ) .fst))
  pt x = ⇔toPath (fwd x) (bwd x)

step-table : IsOrd ((lookup b γ) .fst)
           → Values (lookup f γ) ((lookup b γ) .fst)
           → Entries (lookup f γ) ((lookup b γ) .fst)
           → (lookup v γ) .fst ≡ Lset ((lookup b γ) .fst)
           → ⟨ γ ⊨ StepAt v b f ⟩

step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back
  where

  into : (z : S) → ⟨ z .fst ∈ (lookup v γ) .fst ⟩ → ∥ StepOf b f γ z ∥₁
  into z hz = map₁ (below ob ents z)
    (Lset-out ((lookup b γ) .fst) (z .fst)
      (subst (λ u → ⟨ z .fst ∈ u ⟩) q hz))

  back : (z : S) → StepOf b f γ z → ⟨ z .fst ∈ (lookup v γ) .fst ⟩
  back z s = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym q) (above vals z s)

逆に、証人は above によって z を塔の中に置き、輸送は q に沿って逆向きに走る。

近似が記録するすべての値

帰納は一回、入力の上で、メタ言語の中で行われる。近似とその定義域は固定したままである。動機はこう言う。近似がこの入力で記録するどんな値も、メタレベルの塔のそこでの値に等しい、と。動機は記録されたすべての値を量化する。だから一価性がどこにも仮定として現れないのである。同じ入力で記録された二つの値は、どちらも同じ塔の値に釘づけになり、等しくなる。記録された値の一意性は、仮定ではなく帰納から読み出される。

帰納のステップは、記録された値に対する step-Lset である。入力の下での正しさは、そのまま逐語的に帰納の仮定である。入力の下での完備さを使うのが、近似の値の条項を費やす場所である。この入力より下の入力は近似の定義域の下にもある。定義域は順序数であり、順序数は推移的だからである。だから近似はそこで値を持ち、帰納の仮定がそれを塔の値と同一視する。その値は「単に」取り出されるだけで十分である。それについて証明するのは一つの所属だからである。

module _ {n : ℕ} (f a : Fin n) (γ : Vec S n) where

private
  Value : V ℓ → Type (ℓ-suc ℓ)
  Value u = ⟨ isL u ⟩ → (z : S)
          → ⟨ pr u (z .fst) ∈ (lookup f γ) .fst ⟩ → z .fst ≡ Lset u

approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd ((lookup a γ) .fst)
           → (x z : S) → ⟨ pr (x .fst) (z .fst) ∈ (lookup f γ) .fst ⟩
           → z .fst ≡ Lset (x .fst)
approx-val h oa x = ∈-induction {P = Value} go (x .fst) (x .snd)

  where
  go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
  go u IH hu z p = step-Lset zero (suc zero) (sh2 f) (z ∷ d ∷ γ)
    (ApproxAt-step f a γ h d z p) ou vals ents

    where
    d : S
    d = u , hu
    u∈a : ⟨ u ∈ (lookup a γ) .fst ⟩
    u∈a = ApproxAt-dom f a γ h d z p

    ou : IsOrd u
    ou = mem-ord {A = (lookup a γ) .fst} oa u u∈a

    vals : Values (lookup f γ) u
    vals c y c∈ q = IH (c .fst) c∈ (c .snd) y q

    ents : Entries (lookup f γ) u
    ents c c∈ = rec₁
      ((pr (c .fst) (Lset (c .fst)) ∈ (lookup f γ) .fst) .snd) named
      (ApproxAt-value f a γ h c (oa .fst {x = u} {y = c .fst} c∈ u∈a))

      where
      named : Σ[ y ∶ S ] ⟨ pr (c .fst) (y .fst) ∈ (lookup f γ) .fst ⟩
            → ⟨ pr (c .fst) (Lset (c .fst)) ∈ (lookup f γ) .fst ⟩
      named (y , q) = subst (λ t → ⟨ pr (c .fst) t ∈ (lookup f γ) .fst ⟩)
        (IH (c .fst) c∈ (c .snd) y q) q

単に与えられただけの記録された値は、帰納の仮定によって塔と同定される。輸送の後には、正準な項目が記録されている。完備さが求めるのはこれである。

グラフは正しい値だけを認める

塔のグラフは、枠での値が入力での塔の値であると言う。そしてそれを、近似を通して言う。入力でのステップがその値であるような近似が、単に存在する、と。ほどけば、必要な材料はすべて手もとにある。入力の下での正しさは、今完了した帰納から来る。入力の下での完備さは、近似の値の条項から来て、同じ帰納によって運ばれる。最後にもう一度 step-Lset を適用すれば、記録された値は塔と同定される。ゆえにグラフはその値を決定する。順序数でそれを満たすものは何であれ、メタレベルの塔のそこでの値である。

この読みが変数の枠の上に立つのは飾りではない。実例化はそれぞれ異なる具体的な環境に住み、一方で述べた主張を他方へ運ぶには、全体の塔の記述を内側に抱えた充足を通さねばならない。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

Lset-only : ⟨ γ ⊨ LsetGraphAt w b ⟩ → IsOrd ((lookup b γ) .fst)
          → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)

Lset-only h ob = rec₁
  (setIsSet ((lookup w γ) .fst) (Lset ((lookup b γ) .fst))) read
  (LsetGraph-out w b γ h)
  where

  read : GraphOf w b γ → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)
  read (f , (ha , hs)) =
    step-Lset (suc w) (suc b) zero (f ∷ γ) hs ob vals ents

    where
    vals : Values f ((lookup b γ) .fst)
    vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p

    ents : Entries f ((lookup b γ) .fst)
    ents c c∈ = rec₁ ((pr (c .fst) (Lset (c .fst)) ∈ f .fst) .snd) named
      (ApproxAt-value zero (suc b) (f ∷ γ) ha c c∈)

      where
      named : Σ[ y ∶ S ] ⟨ pr (c .fst) (y .fst) ∈ f .fst ⟩
            → ⟨ pr (c .fst) (Lset (c .fst)) ∈ f .fst ⟩
      named (y , q) = subst (λ t → ⟨ pr (c .fst) t ∈ f .fst ⟩)
        (approx-val zero (suc b) (f ∷ γ) ha ob c y q) q

単に与えられただけの記録された値は、同じ帰納によってもう一度塔と同定され、輸送の後に記録されているのは正準な項目ちょうどである。

表は近似である

逆方向には証人が要るが、正しくて完備な表がまさにそれである。graph-table は、そのような表を塔のグラフの充足に変える。前章の条項を埋めるだけで、それ以上のことは何もしない。

近似の定義域の連言は、入力が定義域にあるという二つの言い方の間の同値であり、Domain と Entries がその二方向を証明する。c で記録された項目が c を界の下へ置き、c が界の下にあるときには c での正準な項目が記録される。記録された組 (c, y) でのステップの連言は、c に対する step-table である。順序数の推移性が、表の正しさと完備さを c の下の入力へ制限する。ステップの補題がそこで消費するのはこれである。グラフが問う値は入力全体でのステップであり、これも step-table が、記録された値と塔の同定を入力にして与える。

主張は、表 h、入力の順序数性、入力の上での表の三条件、そして記録された値が塔であるという主張を受け取る。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

graph-table : (h : S) → IsOrd ((lookup b γ) .fst)
            → Values h ((lookup b γ) .fst) → Entries h ((lookup b γ) .fst)
            → Domain h ((lookup b γ) .fst)
            → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)

            → ⟨ γ ⊨ LsetGraphAt w b ⟩
graph-table h ob vals ents dom q = LsetGraph-in w b γ h approx
  (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents q)
  where

  onDom : (c : S)
        → (⟨ ∃[ y ∶ S ] pr (c .fst) (y .fst) ∈ h .fst ⟩
           → ⟨ c .fst ∈ (lookup b γ) .fst ⟩)
        × (⟨ c .fst ∈ (lookup b γ) .fst ⟩
           → ⟨ ∃[ y ∶ S ] pr (c .fst) (y .fst) ∈ h .fst ⟩)

  onDom c = (λ hy → rec₁ ((c .fst ∈ (lookup b γ) .fst) .snd) named hy)
          , (λ c∈ → ∣ LsetS (c .fst) (mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈)
                   , ents c c∈ ∣₁)

    where
    named : Σ[ y ∶ S ] ⟨ pr (c .fst) (y .fst) ∈ h .fst ⟩
          → ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    named (y , p) = dom c y p

  onStep : (c y : S) → ⟨ pr (c .fst) (y .fst) ∈ h .fst ⟩
         → ⟨ (y ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
  onStep c y p = step-table zero (suc zero) (suc (suc zero)) (y ∷ c ∷ h ∷ γ)
    oc vals' ents' (vals c y c∈ p)

    where
    c∈ : ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    c∈ = dom c y p
    oc : IsOrd (c .fst)
    oc = mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈

    vals' : Values h (c .fst)
    vals' e t _ r = vals e t (dom e t r) r
    ents' : Entries h (c .fst)
    ents' e e∈ = ents e (ob .fst {x = c .fst} {y = e .fst} e∈ c∈)

  approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
  approx = ApproxAt-in zero (suc b) (h ∷ γ)
    (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep

二つの連言を組み立てると、表そのものが近似になる。定義域の条項が今証明した同値であり、ステップの条項がその前のものである。正しくて完備な表が入力の下の階層の記録を含む、と言うのはこの意味である。

順序対のグラフ

表は作られなければならない。L の内側で使える作り手は置換だけであり、置換はグラフを要求する。置換は、関数グラフの記述のあとで表を集める。表の項目は入力 c と値 z の順序対であり、z が c での塔のグラフを満たすとき、グラフはその項目について成立する。塔が渡り歩く台は定数に固定されている。一つの存在量化が塔の値を束縛し、対の読み出しが項目を「入力と束縛された値」の対と等置し、塔のグラフが、束縛された値が正しいことを言う。

この二つの読み出しは、文をパラメータとして受け取り、文自身の等式を仮定として受け取る。本章の呼び出しでは refl である。枠組みは文に対して一般的である。渡された論理式が何であれ、それが順序対のグラフを綴っているという仮定のもとで、読み出しは語る。等式は文とともに渡されるので、読み出しの適用にそれ以上の議論は要らない。

内部の階層

Recorded は、α における内部の階層が集めるべきクラスに名前を与える。基礎の集合が α の下にある入力 c と、塔の c での値の対であり、そのほかには何もない。IsHier は、モデルのある集合がこのクラスを要素ごとに実現することを言う。台の要素 z それぞれに対し、その集合への所属は、z がそのような対を提示するときにちょうど成立する。この主張の両方向が使われる。HierOf は、実現する集合をその仕様とともに集める。構成が作るのはこの形であり、二つの読み出しが消費するのもこの形である。

二つの読み出しは、仕様を通して届く変数の実現集合の上に立つ。これから作る構成が、自分の作っている集合にそれを適用できるようにするためである。外向きの読みは、階層の対の単射性をある要素に適用する。実現集合の項目は、B の下の入力と塔のそこでの値を名指す。内向きの読みは、正準な対をモデルの要素として示す。これはモデル自身の対の構成が与えるが、入力の順序数性も要る。それがなければ、塔のそこでの値をそもそも名指せないからである。

そして構成である。順序数の上の、所属に沿う帰納が一回。α において、対のグラフは下のすべての入力で関数的である。帰納の仮定がその入力までの階層を渡し、graph-table がそれを塔のグラフの充足に変え、Lset-only がそれを満たすものはほかにないと言う。置換が対をモデルの集合に集める。各入力の順序数性は mem-ord から来て、関数性の要求は mereFunct で満たされる。入力での値は判定ではなく構成だからである。

Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Recorded B z = ∃[ c ∶ S ] (c .fst ∈ B)
  ⊓ ((z ≡ pr (c .fst) (Lset (c .fst))) , setIsSet z (pr (c .fst) (Lset (c .fst))))

Recorded B z は命題であり、こう言う。基礎の集合が B の下にある台の要素 c のうち何かに対して、z の基礎の集合は c .fst と塔の c での値の順序対である、と。二つの h-集合の等しさはそれ自体命題なので、これは命題の上での選言の集まりである。

IsHier : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
IsHier B h = (z : S) → (z .fst ∈ h .fst) ≡ Recorded B (z .fst)

IsHier B h は、h が提示する集合が、記録されたクラスを要素ごとに実現することを言う。各 z で、集合への所属と記録されていることは同じ命題である。どちらの方向も捨てられない。それぞれに使い道があるからである。所属だけがあればよしとすると、よそ者が入る。記録だけがあればよしとすると、あるべき対が抜け落ちる。

HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
HierOf B = Σ[ h ∶ S ] IsHier B h

HierOf B は、実現する集合をその仕様とともに集める。この対こそ、帰納がそれぞれの順序数で作るものであり、その二つの成分は、構成に対して誰もが問う二つの問いに答える。それは何か。なぜそれが資格をもつのか。

module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where

hier-out : (c z : S) → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩
         → ⟨ c .fst ∈ B ⟩ × (z .fst ≡ Lset (c .fst))

hier-out c z p = rec₁
  (isProp× ((c .fst ∈ B) .snd) (setIsSet (z .fst) (Lset (c .fst)))) read
  (subst ⟨_⟩ (sp k) p)
  where

  k : S
  k = pr (c .fst) (z .fst)
    , isL-trans {x = h .fst} {y = pr (c .fst) (z .fst)} p (h .snd)

  read : Σ[ d ∶ S ] (⟨ d .fst ∈ B ⟩
           × (pr (c .fst) (z .fst) ≡ pr (d .fst) (Lset (d .fst))))
       → ⟨ c .fst ∈ B ⟩ × (z .fst ≡ Lset (c .fst))
  read (d , (d∈ , eq)) =
      subst (λ t → ⟨ t ∈ B ⟩) (sym (pr-inj eq .fst)) d∈

    , (pr-inj eq .snd ∙ cong Lset (sym (pr-inj eq .fst)))

hier-in : (c : S) → ⟨ c .fst ∈ B ⟩ → ⟨ pr (c .fst) (Lset (c .fst)) ∈ h .fst ⟩
hier-in c c∈ = subst (λ t → ⟨ t ∈ h .fst ⟩) (prʟ-fst c (LsetS (c .fst) oc))
  (subst ⟨_⟩ (sym (sp k)) ∣ c , (c∈ , prʟ-fst c (LsetS (c .fst) oc)) ∣₁)

  where
  oc : IsOrd (c .fst)
  oc = mem-ord {A = B} oB (c .fst) c∈
  k : S
  k = prʟ c (LsetS (c .fst) oc)

c の順序数性は B の順序数性から来る。それがあってはじめて、塔の c での値を L の要素として提示でき、モデルの対が第二成分として必要とするのはこれである。

opaque
  hierAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → HierOf α
  hierAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → HierOf α}
    (build (PairGraphAt zero (suc zero)) refl)
    where

帰納のステップ関数は、対のグラフを、自分自身の等式を携えた変数の文として保つ。実例化先の閉じた文を書き出すのではない。等式は文とともに渡されるので、以下のどの読み出しも呼び出しで refl を仮定として受け取る。

    build : (φ : Formula S ) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ)
          → ⟨ isL α ⟩ → IsOrd α → HierOf α

ステップは、文とその等式、順序数 α、その二つの証明書、そして帰納の仮定を受け取る。α のすべての要素で階層はすでに作られている。ステップは、α での階層とその仕様を返さねばならない。

    build φ qφ α IH hα oα = r .fst .fst , spec
      where
      A : S
      A = α , hα

α での階層は、実現者の第一成分であり、置換がそれを作ったのちに一度取り出される。A は台の要素として提示された α で、置換が定義域を消費する形である。

      value : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      value c c∈ = LsetS (c .fst) (mem-ord {A = α} oα (c .fst) c∈)

      entry : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      entry c c∈ = prʟ c (value c c∈)

α の下では、二つの補助構成がデータに名前を与える。入力 c での値は c での段階であり、段階の提示によって L の要素である。c の順序数性は α の順序数性から来る。c での項目は、モデル自身の「c とその値」の順序対で、記録されたクラスが求める形である。

      below : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) (k : S)
            → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      below c c∈ k = graph-table zero (suc (suc zero)) (value c c∈ ∷ k ∷ c ∷ [])
        (hc .fst) oc

塔のグラフは、α の要素 c のために記録された値で成立する。帰納の仮定を費やすのはここである。仮定は c での階層、すなわち入力 c の上で正しくて完備な表を渡す。これは graph-table が求めるものそのものである。環境には、値と、グラフ自身の量化子のための新しい枠と、入力が載る。

        (λ d z _ p → hier-out (c .fst) oc (hc .fst) (hc .snd) d z p .snd)
        (hier-in (c .fst) oc (hc .fst) (hc .snd))
        (λ d z p → hier-out (c .fst) oc (hc .fst) (hc .snd) d z p .fst)
        refl

表の三条件は、c での階層の仕様から読まれる。正しさは、記録されたすべての値が塔のそこでの値であると言い、完備さは正準な項目が記録されると言い、定義域の条件はほかには何も記録されないと言う。最後の引数 refl は、順序対のグラフ自身の等式である。

        where
        oc : IsOrd (c .fst)
        oc = mem-ord {A = α} oα (c .fst) c∈
        hc : HierOf (c .fst)
        hc = IH (c .fst) c∈ (c .snd) oc

c の順序数性は α の順序数性から来る。それがあれば、帰納の仮定は c での階層を、構成可能集合と仕様とともに渡す。

（holds)正準な項目はどれも、順序対のグラフを満たす。c の上のファイバーが示される。そこには、束縛された塔の値、項目をモデルの対と同定する等式、そして値と入力での塔のグラフの充足が入る。証人はファイバーの要素、すなわちグラフの主張が単なる存在を述べる型の要素である。

      holds : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩)
            → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩
      holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ
        (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))

（only)c でグラフを満たすほかのどんな inhabitant も、正準な項目と等しくなる。グラフは、塔の値 z と、(z, c) で成立する塔のグラフへほどける。塔のグラフはその値を決定し、対の単射性が二つの項目を同一視し、等式はこれらのパスの合成である。

      only : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) (k : S)
           → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈
      only c c∈ k h = rec₁ (isSetS k (entry c c∈)) read
        (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)

対の証人は、塔の値 z と、k を「c と z の対」と同定する等式 q に分かれる。基礎の集合が等しければ台の要素は等しい。Σ≡Prop が目標をこれへ帰着させる。

        where
        read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
        read (z , (q , hg)) = Σ≡Prop (λ t → (isL t) .snd)
          ( q

(z, c) での塔のグラフは塔の値を決定する。値・正準な項目・入力を追加した環境で Lset-only を適用すれば、z は塔の c での値である。c の順序数性は α の順序数性から来る。

          ∙ cong (pr (c .fst))
              (Lset-only zero (suc (suc zero)) (z ∷ k ∷ c ∷ []) hg
                (mem-ord {A = α} oα (c .fst) c∈))
          ∙ sym (prʟ-fst c (value c c∈)) )

三つのパスを合成すれば、k は「c と塔の c での値」の対であり、それは自分の定義の読みを通して読んだ正準な項目である。

（fc)c での関数性は、置換が求める可縮なファイバーである。正準な項目がグラフの inhabitant であり、どんな inhabitant もそれと等しくなる。mereFunct が、単なる存在として現れるこの二つの半分を、ちょうどその可縮なファイバーへ組み立てる。

      fc : (c : S) → ⟨ c ∈ˢ A ⟩
         → isContr (Σ[ k ∶ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩)
      fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁

置換がすぐに項目を集める。α の中の入力にわたって、各入力とその一意に定まる値の対がモデルの一つの集合となり、それがその対のクラスをちょうど実現するという主張とともに提示される。α での内部の階層が L の集合として存在する瞬間は、ここである。

      r : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ)))
      r = hasReplacementL A φ fc

      spec : IsHier α (r .fst .fst)
      spec z = ⇔toPath toRec fromRec
        where

残るのは、集められた集合が記録されたクラスを実現することの確認である。仕様は、要素ごとに、収集された集合への所属と、記録された対であることとを比較する。比較の両方向を別々に証明し、各点の同値へ組み合わせる。

        toRec : ⟨ z .fst ∈ (r .fst .fst) .fst ⟩ → ⟨ Recorded α (z .fst) ⟩
        toRec hz = rec₁ squash₁ conv (subst ⟨_⟩ (r .fst .snd z) hz)
          where

収集された集合への所属を外へ読み出す。置換の仕様がそれを、α の要素 c で、c での値が順序対のグラフを満たすという形に変える。消去が正当なのは、記録されたクラスが命題だからである。

          conv : Σ[ c ∶ S ] (⟨ c .fst ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
               → ⟨ Recorded α (z .fst) ⟩
          conv (c , (c∈ , hp)) = ∣ c , (c∈ , cong (λ p → p .fst) (only c c∈ z hp)
                                            ∙ prʟ-fst c (value c c∈)) ∣₁

証人に対しては、一意性が、c で記録された値が正準な項目に等しいと言い、正準な項目はモデルの「c と塔の c での値」の対に等しくなる。基礎の集合がそれに従い、これが「記録されている」ことの要求そのものである。

        fromRec : ⟨ Recorded α (z .fst) ⟩ → ⟨ z .fst ∈ (r .fst .fst) .fst ⟩
        fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (map₁ conv hz)
          where

内側へ読む。記録された対は、α の下の入力と塔のそこでの値を示す。順序対のグラフはその入力の正準な項目で成立し、収集された集合はその項目を含む。

          conv : Σ[ c ∶ S ] (⟨ c .fst ∈ α ⟩
                   × (z .fst ≡ pr (c .fst) (Lset (c .fst))))
               → Σ[ c ∶ S ] (⟨ c .fst ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)

証人は、記録された提示からグラフの提示へ変換される。入力はそのままで、基礎の集合が典型的な対と等しいという等式が、そこでの順序対のグラフの充足になる。

          conv (c , (c∈ , eq)) = c , (c∈
            , subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩) (sym zeq) (holds c c∈))
            where
            zeq : z ≡ entry c c∈
            zeq = Σ≡Prop (λ t → (isL t) .snd)

この等式は、z が c の正準な項目と同じ集合を提示すると言う。したがって対の要素たちは等しく、holds をこのパスに沿って運べば、z と c での順序対のグラフの充足が得られる。

              (eq ∙ sym (prʟ-fst c (value c c∈)))

hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
hierL α hα oα = hierAt α hα oα .fst

ある順序数での内部の階層とは、帰納が作る実現集合を L の要素として提示したものである。それは構成可能な順序数ごとに存在する。つまり、モデルは今や、自分の各順序数に対して、「その順序数の下の順序数と塔のそこでの値」の順序対をちょうど要素とする集合を含むのである。

hierL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α)
           → IsHier α (hierL α hα oα)
hierL-spec α hα oα = hierAt α hα oα .snd

仕様は構成とともに渡る。帰納が渡す実現集合は、その順序数で IsHier を両方向に満たす。内部の階層のその後のすべての使用は、この説明と照らして検査される。

外部の階層はグラフを満たす

内部の階層は、graph-table と Lset-only によって作られた。それぞれの順序数で、帰納の仮定が下の表を渡し、二つの補題がそれを成立したグラフと一意な値に変える。最後の主張は、今度は逆に走る。仕様 hierL-spec が入力の上での表の条件を渡し、Lset-defines がそれを graph-table に渡す。塔のグラフは記録された値で成立し、隣にある Lset-only は、満たすものがほかにないと言う。こうして内部のグラフとメタレベルの塔は、構成可能な順序数ごとに両方向で一致する。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

Lset-defines : IsOrd ((lookup b γ) .fst)
             → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)
             → ⟨ γ ⊨ LsetGraphAt w b ⟩

Lset-defines ob q = graph-table w b γ H ob
  (λ c z _ p → hier-out ((lookup b γ) .fst) ob H sp c z p .snd)
  (hier-in ((lookup b γ) .fst) ob H sp)
  (λ c z p → hier-out ((lookup b γ) .fst) ob H sp c z p .fst)
  q

  where
  H : S
  H = hierL ((lookup b γ) .fst) (lookup b γ .snd) ob
  sp : IsHier ((lookup b γ) .fst) H
  sp = hierL-spec ((lookup b γ) .fst) (lookup b γ .snd) ob

入力での内部の階層が存在するのは、入力が構成可能な順序数だからである。そしてその仕様は、帰納が証明した所属の同値そのものである。この二つの事実を合わせれば、塔がすべての段階で、モデルの内部に、ほかには何も伴わずに記録されていると言える。

まとめ

approx-val は、入力の上の所属に沿う帰納を一回使って、近似が記録するすべての値がメタレベルの塔のその入力での値に等しいことを証明する。一価性の仮定はどこにもない。同じ入力で記録された二つの値が等しいことは、ここから直接読み出せる。Lset-only と Lset-defines は、グラフと塔の間の二方向であり、後者が hierL を作るときに使われる。hierL はある順序数での内部の階層、L の要素であり、その要素は「その順序数の下の順序数と塔のそこでの値」の順序対ちょうどである。仕様は、帰納が証明した所属の同値である。

ここで表にされる段階は順序数で添字づけられ、順序数は階層の集合である。ホストの宇宙レベルは型の大きさの添字であり、塔の添字になることはない。