環境の塔

module Tower (W : S) where

entry : ℕ → S
entry n = prʟ (numeralL n) (envSet W n)

項目はまず、小さな定義域の原理によって共通の容器に集められる。容器は共有の上界にすぎず、正確な集合は次の分出で刻まれる。

private
  dom : Σ[ d ∶ S ] ((k : Lift {ℓ-zero} {ℓ} ℕ) → ⟨ (entry (lower k)) .fst ∈ d .fst ⟩)
  dom = smallDom (Lift {ℓ-zero} {ℓ} ℕ) (λ k → entry (lower k))

分出に用いる論理式は、候補をアリティと環境集合に分解し、四つの条件を課す。基礎集合の証人が W と等しいこと、候補がそのアリティと環境集合の符号化された順序対であること、アリティが内部の ω に属すること、そしてその集合が W 上の当該アリティの環境集合を表す一階の外延的記述 envSetAt を満たすことである。冒頭の三つの存在量化子は非有界なので、ここでは後の Δ₀ の議論ではなく完全な分出を用いる。

  towerFo : Formula S 
  towerFo = ∃̇ (∃̇ (∃̇ ( (var i2 ≐ con W)
                    ∧̇ ( prAtL i3 i1 i0
                    ∧̇ ( (var i1 ∈̇ con ωʟ)
                    ∧̇ envSetAt i0 i1 i2 )))))

塔は、容器の上の分出によって刻まれ、不透明に保たれる。後の議論は、所属の仕様を通してだけそれを使うのである。

opaque
  tower : S
  tower = hasSeparationL (dom .fst) towerFo .fst .fst

所属の仕様が輸出される。塔の中の所属とは、容器の中の所属と、分出の論理式の充足の連言である。

  tower-mem : (x : S)
            → (x .fst ∈ tower .fst) ≡ ((x .fst ∈ (dom .fst) .fst) ⊓ ((x ∷ []) ⊨ towerFo))
  tower-mem = hasSeparationL (dom .fst) towerFo .fst .snd

重要な材料は、各環境集合がその自身の項目のもとで外延的な記述を満たすことである。環境集合・その数項・台・項目が四つの枠の環境に置かれ、記述は構成によってそこで成立する。

private
  holdsAt : (n : ℕ) → ⟨ (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ []) ⊨ envSetAt i0 i1 i2 ⟩
  holdsAt n = AmbientHolds.holds W (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ [])
                i0 i1 i2 n refl (numeralL-fst n) refl

したがって、すべての正準な項目は塔の中にある。容器への所属は界定の記録から供給され、分出の論理式は、台・数項・環境集合から作られた切り詰められた証人によって充足される。

  tower-in : (n : ℕ) → ⟨ (entry n) .fst ∈ tower .fst ⟩
  tower-in n = subst ⟨_⟩ (sym (tower-mem (entry n)))
    ( dom .snd (lift n)
    , ∣ W , ∣ numeralL n , ∣ envSet W n
      , ( refl

証人の木は、台・構成可能な数項・環境集合を入れ子にし、それぞれの層が自分の成分を運ぶ。順序対は対の射影の法則で認められ、数項の所属は内部の ω の読みで、記述は上の材料によって充足される。

        , ( pr-in i3 i1 i0 (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ [])
              (prʟ-fst (numeralL n) (envSet W n))
          , ( subst ⟨_⟩ (sym (ω-specL (numeralL n))) ∣ lift n , refl ∣₁
            , holdsAt n ))) ∣₁ ∣₁ ∣₁ )

正準な項目は、周囲の標準形で言い直される。構成可能な数項と環境集合の符号化された対の底の順序対は、二つの射影の法則によって、数項と底の段階の対に等しくなる。

tower-in′ : (n : ℕ) → ⟨ pr (# n) ((envSet W n) .fst) ∈ tower .fst ⟩
tower-in′ n = subst (λ u → ⟨ u ∈ tower .fst ⟩)
  (prʟ-fst (numeralL n) (envSet W n) ∙ cong (λ u → pr u ((envSet W n) .fst)) (numeralL-fst n))
  (tower-in n)

逆に、構成した環境の塔の所属を読み出せる。各要素は、ある数項とその長さの環境集合との符号化された順序対であることが命題的切り詰めのもとで得られる。自然数と等式は命題的切り詰めの内側にあるため、この結果は存在を記録するだけで、各要素のアリティを選ぶ関数を定めない。証明はまず所属の仕様を展開し、分出論理式を満たす成分を取り出す。

tower-out : (x : S) → ⟨ x .fst ∈ tower .fst ⟩
          → ∥ Σ[ n ∶ ℕ ] (x .fst ≡ pr (# n) ((envSet W n) .fst)) ∥₁
tower-out x hx = rec₁ squash₁ byB (subst ⟨_⟩ (tower-mem x) hx .snd)
  where
  Goal : Type (ℓ-suc ℓ)

目標の型はこの境界を明示する。自然数 n と、要素の台集合から標準的な順序対 pr (# n) ((envSet W n) .fst) への等式との組を命題的に切り詰めた型である。

  Goal = ∥ Σ[ n ∶ ℕ ] (x .fst ≡ pr (# n) ((envSet W n) .fst)) ∥₁

分出論理式は三つの証人を束縛する。最初の除去で基礎集合の証人 b に名前を付ける。残る論理式はこれを W と同定し、さらにアリティと環境集合の証人を取り出す。

  byB : Σ[ b ∶ S ] ⟨ (b ∷ x ∷ []) ⊨ ∃̇ (∃̇ ( (var i2 ≐ con W)
                  ∧̇ ( prAtL i3 i1 i0
                  ∧̇ ( (var i1 ∈̇ con ωʟ)
                  ∧̇ envSetAt i0 i1 i2 )))) ⟩ → Goal
  byB (b , hb) = rec₁ squash₁ byN hb

二つ目の消去は、アリティを構成可能な集合として名指す。

    where
    byN : Σ[ n ∶ S ] ⟨ (n ∷ b ∷ x ∷ []) ⊨ ∃̇ ( (var i2 ≐ con W)
                  ∧̇ ( prAtL i3 i1 i0
                  ∧̇ ( (var i1 ∈̇ con ωʟ)
                  ∧̇ envSetAt i0 i1 i2 ))) ⟩ → Goal

三つ目の消去は環境集合を名指し、四つの連言支を露わにする。基の集合が W であること、順序対が認められること、アリティが内部の ω に属すること、そして環境集合の外延的な記述が成り立つことである。

    byN (n , hn) = rec₁ squash₁ byE hn
      where
      byE : Σ[ F ∶ S ] ⟨ (F ∷ n ∷ b ∷ x ∷ []) ⊨ ( (var i2 ≐ con W)
                  ∧̇ ( prAtL i3 i1 i0
                  ∧̇ ( (var i1 ∈̇ con ωʟ)

順序対の読み取りにより、要素からアリティと記述された集合との符号化された順序対への等式が得られる。次に、アリティが内部の ω に属することから、同じ台集合をもつ構成可能な数項に対応する通常の自然数が、命題的切り詰めのもとで得られる。

                  ∧̇ envSetAt i0 i1 i2 ))) ⟩ → Goal
      byE (F , (qb , (hp , (hω , hE)))) = rec₁ squash₁ byK (subst ⟨_⟩ (ω-specL n) hω)
        where
        xq : x .fst ≡ pr (n .fst) (F .fst)
        xq = pr-out i3 i1 i0 (F ∷ n ∷ b ∷ x ∷ []) hp

数項の同一視が、記録されたアリティをその自然数の構成可能な数項と整列させ、環境の一致のモジュールが、四つの枠の環境のもとで開かれ、記述された集合と実際に構成された集合を比較する準備をする。

        byK : Σ[ k ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] (n .fst ≡ (numeralL (lower k)) .fst) → Goal
        byK (k , qn) = ∣ lower k , xq ∙ cong₂ pr (qn ∙ numeralL-fst (lower k)) Eq ∣₁
          where
          module Am = Ambient W (F ∷ n ∷ b ∷ x ∷ []) i0 i1 i2 (lower k)
                        (qn ∙ numeralL-fst (lower k)) qb hE using (into; outof)

一致のモジュールは、記述された集合と実際に構成された環境集合の間の所属の両方向を供給する。そして L の内部の外延性が、この二つの方向を、底の集合の等式に変える。

          Eq : F .fst ≡ (envSet W (lower k)) .fst
          Eq = cong (λ p → p .fst) (extensionalL {a = F} {b = envSet W (lower k)}
            (λ z → ⇔toPath (Am.into z) (Am.outof z)))

module EnvFacts (W : S) where

private
  ι : ⟪ W .fst ⟫ → V ℓ
  ι = ⟪ W .fst ⟫↪

提示された索引はどれも W の要素を名指す。小さな所属の橋が、提示から底の集合の中へ続くのである。

  ι∈ : (q : ⟪ W .fst ⟫) → ⟨ ι q ∈ W .fst ⟩
  ι∈ q = ∈∈ₛ {a = ι q} {b = W .fst} .snd (∈ₛ⟪ W .fst ⟫↪ q)

長さゼロの索引はちょうど一つであり、それは、空の型からの関数がその不可能な場合によって定義されることから認められる。

  g0 : Ix W 
  g0 ()

要素をもたない集合は、長さゼロの環境のグラフと等しくなる。外延性による。長さゼロの索引には場合がないので、どちらの側にも要素はないのである。

noMembers→env0 : (z : V ℓ) → ((y : V ℓ) → ⟨ y ∈ z ⟩ → ⊥₀) → z ≡ (envS W g0) .fst
noMembers→env0 z k = extensionalV (λ y → ⇔toPath
  (λ hy → ⊥₀-rec (k y hy))
  (rec₁ ((y ∈ z) .snd) (λ { (lift () , _) })))

逆に、長さゼロのどの環境のグラフも要素をもたない。索引に場合がないので、要素を符号化する対が作れないのである。

envAny0-noMembers : (g : Ix W ) (y : V ℓ) → ⟨ y ∈ (envS W g) .fst ⟩ → ⊥₀
envAny0-noMembers g y = rec₁ isProp⊥ (λ { (lift () , _) })

長さゼロの環境集合を読み出すと、そのすべての要素は要素をもたない集合である。証明は、切り詰められた提示を消去して、前の事実を適用する。

envSet0-out : (z : V ℓ) → ⟨ z ∈ (envSet W ) .fst ⟩
            → (y : V ℓ) → ⟨ y ∈ z ⟩ → ⊥₀
envSet0-out z hz y hy = rec₁ isProp⊥
  (λ { (g , e) → envAny0-noMembers g y (subst (λ u → ⟨ y ∈ u ⟩) e hy) })
  (envSet-out W  (down (envSet W ) z hz) hz)

長さゼロの環境集合の埋めは空集合を使う。それは提示の中へ運ばれ、空のグラフはその要素がないことの証明によって認められる。

envSet0-in : (z : V ℓ) → ((y : V ℓ) → ⟨ y ∈ z ⟩ → ⊥₀) → ⟨ z ∈ (envSet W ) .fst ⟩
envSet0-in z k = subst (λ u → ⟨ u ∈ (envSet W ) .fst ⟩) (sym (noMembers→env0 z k)) (envSet-in W g0)

環境の符号化は、関数の水準で cons と一致する。台の要素を先頭に加え、索引をずらすと、符号化された関数の cons を項目ごとにちょうど符号化するのである。

cons-env : (q : ⟪ W .fst ⟫) {k : ℕ} (g : Ix W k)
         → env (cons (ι q) (λ i → ι (g i))) ≡ (envS W (cons q g)) .fst
cons-env q g = cong env (funExt (λ { zero → refl ; (suc i) → refl }))

台 W のすべての要素は、長さ k のどの環境も、長さ suc k の環境へ延長する。W の新しい要素は索引で提示され、延長された関数が、後続の環境集合の中に挿入される。

envCons∈ : {k : ℕ} (x : V ℓ) → ⟨ x ∈ W .fst ⟩ → (g : Ix W k)
         → ⟨ env (cons x (λ i → ι (g i))) ∈ (envSet W (suc k)) .fst ⟩
envCons∈ {k} x x∈ g =
  subst (λ u → ⟨ u ∈ (envSet W (suc k)) .fst ⟩)
    (sym (cong (λ v → env (cons v (λ i → ι (g i)))) (sym (fib .snd)) ∙ cons-env (fib .fst) g))

提示の索引は、その要素における提示の繊維を通して復元されるので、符号化は x の実際の提示の索引を使う。

    (envSet-in W (cons (fib .fst) g))
  where
  fib : Σ[ q ∶ ⟪ W .fst ⟫ ] (ι q ≡ x)
  fib = ∈-asFiber {a = x} {b = W .fst} x∈

この挿入は、底の集合の同一視をもつ構成可能な要素に対して言い直される。その同一視に沿って運ぶことで、後続の環境集合への所属が従う。

envSuc-in : {k : ℕ} (x e' : S) → ⟨ x .fst ∈ W .fst ⟩ → (g : Ix W k)
          → e' .fst ≡ env (cons (x .fst) (λ i → ι (g i)))
          → ⟨ e' .fst ∈ (envSet W (suc k)) .fst ⟩
envSuc-in {k} x e' x∈ g qe' =
  subst (λ u → ⟨ u ∈ (envSet W (suc k)) .fst ⟩) (sym qe') (envCons∈ (x .fst) x∈ g)

後続の環境は、関数のレベルで先頭と尾部に分かれる。g' が後続の環境に添字づけられているなら、その基礎の集合は、零番目の項目が ι (g' zero)、第 i+1 項目が ι (g' (suc i)) であるような符号化されたグラフと等しくなる。証明は、二つの添字の関数がすべての枠で同じ値をもつという関数外延性のもとでの、環境の構成子の関数性による。

env-split : {k : ℕ} (g' : Ix W (suc k))
          → (envS W g') .fst ≡ env (cons (ι (g' zero)) (λ i → ι (g' (suc i))))
env-split g' = cong env (funExt (λ { zero → refl ; (suc i) → refl }))

後続環境の外向きの読み出しが先頭と尾部を復元するのは、命題的切り詰めのもとでだけである。envSet W (suc k) の各要素 e' に対して、W の要素 ι q を名指す表示添字 q、尾部の添字 g : Ix W k、および e' の基礎の集合を両者の cons 関数の符号化グラフと同定する等式が単に存在する。

envSuc-out : {k : ℕ} (e' : S) → ⟨ e' .fst ∈ (envSet W (suc k)) .fst ⟩
           → ∥ Σ[ q ∶ ⟪ W .fst ⟫ ] Σ[ g ∶ Ix W k ]
                (e' .fst ≡ env (cons (ι q) (λ i → ι (g i)))) ∥₁
envSuc-out {k} e' h = map₁
  (λ { (g' , e) → g' zero , (λ i → g' (suc i)) , (e ∙ env-split g') })

所属の証明は、環境の集合の外向きの読み出しに消費され、切り詰められた添字を供給する。グラフの等式は、分かちの補題と合成されて、cons の等式を作る。

  (envSet-out W (suc k) e' h)

module ConsImageRead {m : ℕ} (F' F w : Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) where

open EnvFacts W
private
  ι : ⟪ W .fst ⟫ → V ℓ

台から階層への埋め込みは一度だけ名づけられ、符号化が必要とするときに、台のすべての要素を階層の要素として提示できるようにする。

  ι = ⟪ W .fst ⟫↪

W の台の各 q に対して、提示写像は ι q を W の基礎の集合に入れる。証明は、その集合の標準的な提示が与えるファイバーから所属を読み取る。

  ι∈' : (q : ⟪ W .fst ⟫) → ⟨ ι q ∈ W .fst ⟩
  ι∈' q = ∈∈ₛ {a = ι q} {b = W .fst} .snd (∈ₛ⟪ W .fst ⟫↪ q)

cons の像の条項の外向きの読み出しはこう言う。基底の集合が k での段階の環境の集合に等しいなら、cons の像の条項を満たす集合は、後続の段階の環境の集合に等しい、と。証明は、二方向で要素を比較する外延性である。

前向きの方向は、cons の像の条項を通して、候補の後続の集合の要素 z を読む。

consImage-out : (k : ℕ) → (lookup F γ) .fst ≡ (envSet W k) .fst
              → ⟨ γ ⊨ consImage F' F w ⟩ → (lookup F' γ) .fst ≡ (envSet W (suc k)) .fst
consImage-out k qF (h1 , h2) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
  where
  fwd : (z : V ℓ) → ⟨ z ∈ (lookup F' γ) .fst ⟩ → ⟨ z ∈ (envSet W (suc k)) .fst ⟩

条項は、台の要素 x と、符号化された環境の項目 e と、cons の等式を供給する。基底の集合の環境の集合の外向きの読み出しが、切り詰められた添字 g を供給する。それぞれの切り詰められた証人は、つぎの命題へ消去される。

  fwd z hz = rec₁ ((z ∈ (envSet W (suc k)) .fst) .snd)
    (λ { (x , (x∈ , hx)) → rec₁ ((z ∈ (envSet W (suc k)) .fst) .snd)
      (λ { (e , (e∈ , hc)) → rec₁ ((z ∈ (envSet W (suc k)) .fst) .snd)
        (λ { (g , qe) →
          envSuc-in x zS (subst (λ u → ⟨ x .fst ∈ u ⟩) qw x∈) g

前向きの包含では、cons 像の条項の前半が、先頭 x、尾部の環境 e、および符号化された cons 関係の充足を与える。e を実際の基底環境集合の要素として読むと、命題的切り詰めのもとで尾部の添字が得られる。次に consAtL の妥当性が z を意味論的な cons グラフと同定し、envSuc-in がそのグラフを envSet W (suc k) に入れる。どの切り詰めも、この所属命題にだけ除去される。

            (subst ⟨_⟩ (consAtL-adequate i2 i1 i0 (e ∷ x ∷ zS ∷ γ) (λ i → ι (g i)) qe) hc) })
        (envSet-out W k e (subst (λ u → ⟨ e .fst ∈ u ⟩) qF e∈)) })
      hx })
    (h1 zS hz)
    where

z が候補の後続集合に属するという証明から、基礎の集合が z である構成可能な代表 zS : S が得られる。この代表を有界な cons 像の読み手に渡す。

    zS : S
    zS = down (lookup F' γ) z hz

逆向きの包含を示すため、実際の後続環境集合の要素 z を取る。その後続分解は、先頭 q、尾部の添字 g、および z を両者の cons 環境と同定する等式が単に存在することを与える。次に cons の像の条項の後半から、候補の後続集合の対応する要素 e' が単に存在することを得る。

  bwd : (z : V ℓ) → ⟨ z ∈ (envSet W (suc k)) .fst ⟩ → ⟨ z ∈ (lookup F' γ) .fst ⟩
  bwd z hz = rec₁ ((z ∈ (lookup F' γ) .fst) .snd)
    (λ { (q , g , qz) → rec₁ ((z ∈ (lookup F' γ) .fst) .snd)
      (λ { (e' , (e'∈ , hc)) →
        subst (λ u → ⟨ u ∈ (lookup F' γ) .fst ⟩)

consAtL の妥当性により、条項が与える対象言語の cons 関係は、意味論的な分解で使われたものと同じ符号化 cons グラフに同定される。この等式を分解の等式と合成すると e' と z が同定されるので、e' の所属を z の所属へ移せる。

          (subst ⟨_⟩ (consAtL-adequate i0 i1 i2 (e' ∷ xS q ∷ envS W g ∷ γ) (λ i → ι (g i)) refl) hc
           ∙ sym qz)
          e'∈ })
      (h2 (envS W g) (subst (λ u → ⟨ (envS W g) .fst ∈ u ⟩) (sym qF) (envSet-in W g))
          (xS q) (subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q))) })

二つの命題截断はいずれも、証明中の所属命題にだけ消去される。zS は z を構成可能な台の中で提示し、xS は復元された先頭を同様に提示する。

    (envSuc-out zS hz)
    where
    zS : S
    zS = down (envSet W (suc k)) z hz
    xS : ⟪ W .fst ⟫ → S

復元された先頭 q について、その像 ι q は W に属する。したがって構成可能性の推移性から、台の要素 xS q を作るために必要な証明が得られる。

    xS q = ι q , isL-trans {x = W .fst} {y = ι q} (ι∈' q) (W .snd)

cons の像の条項の内向きの方向は、実際の段階の環境の集合との二つの同定から証明される。これで、cons の像の条項の両方向が使える。

consImage-in : (k : ℕ) → (lookup F γ) .fst ≡ (envSet W k) .fst
             → (lookup F' γ) .fst ≡ (envSet W (suc k)) .fst
             → ⟨ γ ⊨ consImage F' F w ⟩
consImage-in k qF qF' = h1 , h2
  where

内向きの読み出しの最初の方向は、候補の後続の集合のすべての要素が有界の存在量化子を満たすと言う。先頭の要素と、基底の集合からの環境が存在し、その cons の拡張がその要素になる、というものである。要素の切り詰められた分解を消費して、先頭と尾部を名指す。

  h1 : (e' : S) → ⟨ e' .fst ∈ (lookup F' γ) .fst ⟩
     → ⟨ (e' ∷ γ) ⊨ ∃̇∈ (var (sh  w)) (∃̇∈ (var (sh  F)) (consAtL i2 i1 i0)) ⟩
  h1 e' he' = map₁
    (λ { (q , g , qe') →
      let xS : S

先頭は台の中へ載せられ、尾部は基底の集合への所属の同定によって基底の集合の要素として提示され、cons の妥当性が cons の等式を対象言語の中へ運ぶ。

          xS = ι q , isL-trans {x = W .fst} {y = ι q} (ι∈' q) (W .snd)
      in xS , ( subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q)
            , ∣ envS W g , ( subst (λ u → ⟨ (envS W g) .fst ∈ u ⟩) (sym qF) (envSet-in W g)
                           , subst ⟨_⟩ (sym (consAtL-adequate i2 i1 i0 (envS W g ∷ xS ∷ e' ∷ γ) (λ i → ι (g i)) refl)) qe' ) ∣₁ ) })
    (envSuc-out e' (subst (λ u → ⟨ e' .fst ∈ u ⟩) qF' he'))

第二の条項は、基底集合の要素 e とアルファベット集合の要素 x から始まる。ここで必要なのは、e が表す環境の先頭に x を付けて得られる符号化グラフをもつ、候補の後続集合の要素が単に存在することである。

基底環境集合の外向きの読み出しから尾部の添字 g が単に存在することを得て、意味論的な cons の導入によって、得られたグラフを実際の後続環境集合に入れる。

  h2 : (e : S) → ⟨ e .fst ∈ (lookup F γ) .fst ⟩ → (x : S) → ⟨ x .fst ∈ (lookup w γ) .fst ⟩
     → ⟨ (x ∷ e ∷ γ) ⊨ ∃̇∈ (var (sh  F')) (consAtL i0 i1 i2) ⟩
  h2 e he x hx = map₁
    (λ { (g , qe) →
      let m : ⟨ env (cons (x .fst) (λ i → ι (g i))) ∈ (envSet W (suc k)) .fst ⟩

作られた環境は、cons の導入が供給する所属を下降して、後続の段階の環境の集合の要素として提示される。cons の妥当性が、cons の条項の充足を対象言語の中へ運ぶ。

          m = envCons∈ (x .fst) (subst (λ u → ⟨ x .fst ∈ u ⟩) qw hx) g
          e' : S
          e' = down (envSet W (suc k)) (env (cons (x .fst) (λ i → ι (g i)))) m
      in e' , ( subst (λ u → ⟨ e' .fst ∈ u ⟩) (sym qF') m
              , subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i2 (e' ∷ x ∷ e ∷ γ) (λ i → ι (g i)) qe)) refl ) })

基底の集合の外向きの読み出しが、切り詰められた添字 g を供給する。その環境が項目 e である。

    (envSet-out W k e (subst (λ u → ⟨ e .fst ∈ u ⟩) qF he))

module SglEmpty (W : S) {m : ℕ} (F : Fin m) (γ : Vec S m) where

open EnvFacts W

一つの空集合の条項の外向きの読み出しは、その条項を満たす集合が、零の段階の環境の集合と同じ基礎の集合をもつと言う。証明は、二方向で要素を比較する外延性である。

最初に名づけられた対象は、候補の基礎の集合であり、none の補助が、有界の条項から反駁を取り出す。

sglEmpty-out : ⟨ γ ⊨ sglEmpty F ⟩ → (lookup F γ) .fst ≡ (envSet W ) .fst
sglEmpty-out (hex , hall) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
  where
  Fv = (lookup F γ) .fst
  none : (z : S) → ⟨ (z ∷ γ) ⊨ emptyAll i0 ⟩ → (y : V ℓ) → ⟨ y ∈ z .fst ⟩ → ⊥₀

none の補助は、要素の台の提示を有界の条項に渡す。条項は空型を返し、提示された集合に要素がないことを確かめる。

  none z k y hy = ⊥*-rec (k (down z y hy) hy)

前向き：候補の集合の要素が提示され、有界の条項がそのすべての要素を反駁するので、要素をもたない。零の段階の導入が、それを零の段階の環境の集合の要素として受け入れる。

  fwd : (z : V ℓ) → ⟨ z ∈ Fv ⟩ → ⟨ z ∈ (envSet W ) .fst ⟩
  fwd z hz = envSet0-in z (none (down (lookup F γ) z hz) (hall (down (lookup F γ) z hz) hz))

後ろ向き：零の段階の環境の集合の要素が提示され、その切り詰められた添字が消費される。添字づけられた環境とその要素の両方が要素をもたないことが示されるので、階層の外延性によって両者は等しくなる。

  bwd : (z : V ℓ) → ⟨ z ∈ (envSet W ) .fst ⟩ → ⟨ z ∈ Fv ⟩
  bwd z hz = rec₁ ((z ∈ Fv) .snd)
    (λ { (e , (e∈ , he)) →
      subst (λ u → ⟨ u ∈ Fv ⟩)
        (noMembers→env0 (e .fst) (none e he) ∙ sym (noMembers→env0 z (envSet0-out z hz)))

運ばれた所属が後ろ向きの方向を閉じ、存在の条項が、候補が空でないことを確かめて、証明を完成させる。

        e∈ })
    hex

内向きの読み出しでは、空の環境 e0 を選ぶ。e0 は零段階の環境集合に属し、要素をもたないので、存在の側が成り立つ。また、その環境集合のどの要素も要素をもたないので、全称の側も成り立つ。仮定された等式に沿って移送することで、両方に現れる実際の零段階集合を候補集合に置き換える。

sglEmpty-in : (lookup F γ) .fst ≡ (envSet W ) .fst → ⟨ γ ⊨ sglEmpty F ⟩
sglEmpty-in q =
    ∣ e0 , ( subst (λ u → ⟨ e0 .fst ∈ u ⟩) (sym q) (envSet-in W (λ ()))
           , (λ y hy → lift (envAny0-noMembers (λ ()) (y .fst) hy)) ) ∣₁
  , (λ z hz y hy → lift (envSet0-out (z .fst) (subst (λ u → ⟨ z .fst ∈ u ⟩) q hz) (y .fst) hy))

空の環境は、空型からの関数の符号化されたグラフであり、項目をもたない。

  where
  e0 : S
  e0 = envS W (λ ())

module TowerRead {m : ℕ} (E w N0 : Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (qN0 : (lookup N0 γ) .fst ≡ # )
  (h : ⟨ γ ⊨ towerAt E w N0 ⟩) where

private
  Ev = (lookup E γ) .fst

塔の論理式の三つの連言項に名前がつけられる。基底の条項、上向きの閉じの条項、そして下向きの分解の条項である。

  hbase = h .fst
  hup = h .snd .fst
  hdown = h .snd .snd

項目とは、自然数のアリティと、そのアリティで提示される環境の集合の、切り詰められた記録である。塔の外向きの方向の読みの目標である。

Entry : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Entry n F = ∥ Σ[ k ∶ ℕ ] ((n ≡ # k) × (F ≡ (envSet W k) .fst)) ∥₁

塔の項目の外向きの読み出しは、符号化された対の第一成分の集合についての所属の帰納で証明される。動機はこう言う。階層のすべての要素 nv について、ある項目の第一成分が nv に等しく、その項目が候補の塔に属するなら、その項目は自然数のアリティとその環境の集合に分解される、と。これは、階層の所属関係についての整礎帰納であり、自然数についての通常の帰納ではない。

ステップの関数は、塔の論理式の下向きの分解の条項で場合分けする。

entry-out : (n F : S) → ⟨ pr (n .fst) (F .fst) ∈ Ev ⟩ → Entry (n .fst) (F .fst)
entry-out n F = ∈-induction {P = P} step (n .fst) n F refl
  where
  P : V ℓ → Type (ℓ-suc ℓ)
  P nv = (n F : S) → n .fst ≡ nv → ⟨ pr (n .fst) (F .fst) ∈ Ev ⟩ → Entry (n .fst) (F .fst)

所属の帰納のステップは、塔の論理式の下向きの分解の条項で場合分けする。その対が基底の項目であるか、前の項目をもつかである。

  step : (nv : V ℓ) → ((y : V ℓ) → ⟨ y ∈ nv ⟩ → P y) → P nv
  step nv IH n F qn p∈ = rec₁ squash₁ cases
    (useBoth i0 (pS ∷ γ) n F refl (towerDown E w N0) (hdown pS p∈))
    where
    pS : S

候補の順序対の所属証明から、構成可能な代表 pS : S が得られる。その容器は、有界量化を通して数項成分と環境集合成分を公開し、四つのスロットからなる環境は、それらの成分と順序対を本章の外側の環境の前に置く。

    pS = down (lookup E γ) (pr (n .fst) (F .fst)) p∈
    c = container pS n F refl
    δ : Vec S ( + m)
    δ = F ∷ n ∷ c .fst ∷ pS ∷ γ

場合分けは、下向きの分解の充足を消費する。基底の場合は、零の数項の等式と、一つの空集合の条項の外向きの読み出しを読み、アリティ零と零の段階の環境の集合を作る。後続の場合は、再帰のステップに渡される。

    cases : ((n .fst ≡ (lookup N0 γ) .fst) × ⟨ δ ⊨ sglEmpty i0 ⟩)
          ⊎ ⟨ δ ⊨ ∃̇∈ (var (sh  E)) (bothEx i0 (downBody w)) ⟩
          → Entry (n .fst) (F .fst)
    cases (inl (qn0 , hF)) = ∣  , (qn0 ∙ qN0 , SglEmpty.sglEmpty-out W i0 δ hF) ∣₁
    cases (inr hs) = rec₁ squash₁

後続の場合は、有界の存在量化をほどく。前の項目 p' と後続の等式、そして前の数項 n'、前の環境の集合 F'、cons のコンテナと cons の等式である。四つの枠の拡張が帰納を準備する。

順序数の比較は、候補の数項が、前の数項のフォン・ノイマンの後続であると言う。

      (λ { (p' , (p'∈ , hb)) → rec₁ squash₁
        (λ { (n' , F' , s' , (qp' , (hsuc , hci))) →
          let δ' = F' ∷ n' ∷ s' ∷ p' ∷ δ
              qsuc : n .fst ≡ sucV (n' .fst)
              qsuc = suc-out i1 i5 δ' hsuc

前の数項は、そのフォン・ノイマン後続に属し、後続の等式に沿って移送すると、所属に関する帰納法に必要な真の下降が得られる。帰納仮定を適用すれば、アリティ k と段階 envSet W k が復元される。

              n'∈ : ⟨ n' .fst ∈ nv ⟩
              n'∈ = subst (λ u → ⟨ n' .fst ∈ u ⟩) (sym qsuc ∙ qn) (self∈sucV (n' .fst))
          in map₁
            (λ { (k , (qk , qF')) →
              suc k , ( qsuc ∙ cong sucV qk

復元されたアリティはその後続へ写され、cons の像の外向きの読み出しが、基底の環境の集合を後続のものへ運ぶ。帰納の仮定は、塔の等式に沿って所属が運ばれる前の要素で適用される。

                      , ConsImageRead.consImage-out i4 i0 (sh  w) δ' W qw k qF' hci ) })
            (IH (n' .fst) n'∈ n' F' refl
              (subst (λ u → ⟨ u ∈ Ev ⟩) qp' p'∈)) })
        (bothEx-out i0 (downBody w) (p' ∷ δ) hb) })
      hs

内向きの読み出しは、外部の自然数 k に関する通常の帰納法で証明する。零の場合、基底の条項から塔の要素とその第二成分が単に存在することを得る。sglEmpty を読むと第二成分が envSet W 0 に同定され、整合条件 N0 = # 0 によって第一成分も同定される。得られた順序対の等式に沿って移送すれば、標準的な零番目の項目が得られる。

entry-in : (k : ℕ) → ⟨ pr (# k) ((envSet W k) .fst) ∈ Ev ⟩
entry-in  = rec₁ ((pr (# ) ((envSet W ) .fst) ∈ Ev) .snd)
  (λ { (p , (p∈ , hs)) → rec₁ ((pr (# ) ((envSet W ) .fst) ∈ Ev) .snd)
    (λ { (F , s , (qp , hF)) →
      subst (λ u → ⟨ u ∈ Ev ⟩)

零の場合を終えると、後続の場合では、すでに構成した第 k 標準項目に上向き閉包の条項を適用する。この条項から、新しい塔の要素と、後続の論理式を満たす数項、および cons の像の論理式を満たす環境集合が単に存在することを得る。

        (qp ∙ cong₂ pr qN0 (SglEmpty.sglEmpty-out W i0 (F ∷ s ∷ p ∷ γ) hF))
        p∈ })
    (sndEx-out i0 (sh  N0) (sglEmpty i0) (p ∷ γ) hs) })
  hbase
entry-in (suc k) = rec₁ ((pr (# (suc k)) ((envSet W (suc k)) .fst) ∈ Ev) .snd)

後続の論理式は、もとの数項から新しい第一成分を定め、cons 像の論理式の外向きの読みは、envSet W k から新しい第二成分を定める。符号化順序対の等式にこれら二つの同一視を適用すると、標準的な後続項目 (# (suc k), envSet W (suc k)) が得られる。

  (λ { (p' , (p'∈ , hb)) → rec₁ ((pr (# (suc k)) ((envSet W (suc k)) .fst) ∈ Ev) .snd)
    (λ { (n' , F' , s' , (qp' , (hsuc , hci))) →
      let δ' = F' ∷ n' ∷ s' ∷ p' ∷ δ
      in subst (λ u → ⟨ u ∈ Ev ⟩)
           (qp' ∙ cong₂ pr (suc-out i5 i1 δ' hsuc)

帰納仮定はまず、第 k 標準項目の所属を与える。その項目に上向き閉包を適用すると、後続項目とその二つの成分を記述する論理式が、命題的切り詰めのもとで得られる。それらを外向きに読むと、各成分が # (suc k) と envSet W (suc k) に同定されるので、得られた符号化順序対の等式に沿って移送すれば、標準的な後続項目の所属が証明される。

                           (ConsImageRead.consImage-out i0 i4 (sh  w) δ' W qw k refl hci))
           p'∈ })
    (bothEx-out i0 (upBody w) (p' ∷ δ) hb) })
  (useBoth i0 (pS ∷ γ) (nn k) (envSet W k) refl (towerUp E w) (hup pS (entry-in k)))
  where

上向き閉包を使うため、まず第 k 標準項目を台の要素 pS として提示する。そのコンテナが二つの成分を有界量化に公開し、四つの枠からなる環境が、現在の環境集合、数項、コンテナ、塔の項目を順に記録する。

  pS : S
  pS = down (lookup E γ) (pr (# k) ((envSet W k) .fst)) (entry-in k)
  c = container pS (nn k) (envSet W k) refl
  δ : Vec S ( + m)
  δ = envSet W k ∷ nn k ∷ c .fst ∷ pS ∷ γ