---
title: "環境の塔"
module: L.Coding.EnvironmentTower
lang: ja
site: "Bedrock"
description: "環境の塔"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 60
canonical: https://bedrock.institute/ja/L.Coding.EnvironmentTower.html
html: L.Coding.EnvironmentTower.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/EnvironmentTower.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Absoluteness, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.Quantification, L.Coding.EnvironmentSet, L.Coding.EnvironmentAgreement, L.Recursion, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Numerals, L.Axioms.Infinity]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.EnvironmentTower.md, https://bedrock.institute/zh/L.Coding.EnvironmentTower.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
本章では、`L` の内部に環境の塔を構成します。各自然数 `n` に対して、塔は符号化された順序対 `(# n, envSet W n)` を記録します。ここで `envSet W n` は、`W` に値を取る長さ `n` のすべての環境からなる集合です。まず実際の集合を構成し、次に、後の章がその符号化された項目を読み取るための有界な一階記述を与えます。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

この構成は立方型理論の中で行われ、明記された宇宙レベルでの排中律を用います。この古典的仮定は、固定長の環境集合、共通の上界、分出、および内部自然数集合の構成を通して本章に入ります。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

宇宙レベル `ℓ` と実例 `lem : LEM (ℓ-suc ℓ)` を固定します。以下の構成はすべてこの一つの仮定に相対的であり、これより強い古典的原理は加えません。

```agda
module L.Coding.EnvironmentTower {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

本章では、環境の塔について二つの記述を併用します。一つは `L` の集合を外側から構成する記述であり、もう一つは集合論の対象言語における論理式です。後者は所属、等号、連言、選言、有界量化から組み立てられ、Lévy 階層の検査器によって Δ₀ であることが認証されます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ⊥̇; ∃̇_; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
import FOL.Absoluteness
```

後の証明では、塔の項目を先行項目へ向かって下向きに読みます。累積階層の所属帰納がこの降下の整礎性を保証し、外延性が、同じ要素をもつ環境集合を同定します。さらに符号化順序対の単射性によって、数項成分と環境集合成分を別々に復元できます。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env; cons )
```

二つの記述を結ぶのは、符号化順序対、フォン・ノイマン後続、環境集合、cons 拡張を認識する論理式です。容器によって成分をめぐる量化を有界に保ち、妥当性の補題によって、これらの論理式の充足を累積階層の対応する構成と結びます。

```agda
open import L.Coding.Model {ℓ} using ( prAtL; prʟ; prʟ-fst; container )
open import L.Coding.Expressions {ℓ} using
  ( envSetAt; sucAtL; consAtL; consAtL-adequate; numL )
open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; sh; pr-out; pr-in; down; suc-out; suc-in
```

符号化順序対を読んだり構成したりするには、その二成分へ繰り返しアクセスする必要があります。二成分の量化は有界論理式の内部でこのアクセスを与え、その導入・除去補題は充足が命題であることを保ちます。族 `envSet W n` は、それらの成分と比較する意味論的な集合を与えます。

```agda
  ; i4; i5
  ; sndEx; bothEx; bothAll
  ; sndEx-out; bothEx-out; bothAll-in
  ; fillSnd; fillBoth; useBoth )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in; envSet-out; envS; Ix )
```

環境集合の論理式が集合を定めるのは外延的にだけです。その一致定理が、この記述を構成済みの `envSet W n` と比較します。続いて、共通の上界と完全な分出がすべてのアリティを一つの構成可能集合へ集め、構成可能な数項が各項目の第一成分を与えます。

```agda
open import L.Coding.EnvironmentAgreement {ℓ} lem using ( module Ambient; module AmbientHolds )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
```

内部集合 `ωʟ` は、対象言語のアリティを外側の自然数と結びます。その要素を読むと、命題的切り詰めのもとで、自然数と対応する構成可能な数項との同一視が得られます。したがって、何らかのアリティが存在することは分かりますが、各要素に対するアリティを大域的に選ぶことはできません。

```agda
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
```

有限ベクトルは論理式を解釈する環境を表し、依存対と直和は、その意味論が返す証人と場合分けを表します。自然数の加法は、有界な順序対の読み取りによって追加されるスロットを数えます。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.Vec using ( _∷_; []; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
```

本章の意味論的な証人の多くは、命題的切り詰めのもとにあります。所属、充足、階層の集合どうしの等しさのように、目標自身が命題である場合にはその証人を使えますが、そこから大域的に選ばれたアリティや環境を射影することはできません。命題外延性と空型は、それぞれ対応する等式と不可能性の議論を支えます。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
```

累積階層の集合には、その要素の小さな表示が伴います。所属と対応するファイバーの間を移ることで、`W` の任意の要素を表示の添字へ変換できます。同じ階層は、フォン・ノイマン数項 `# n` とその後続演算 `sucV` も与えます。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )
```

構成可能集合の型を `S` と書きます。`S` の要素は、基礎となる階層の集合と、それが `L` に属することの証拠からなります。以下の証明では第一射影を通して基礎の集合を比較し、証人を構成するときには構成可能性の証拠を保ちます。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

論理式の充足は、構成可能集合のベクトルの上で解釈されます。`L` の推移性がこの内部解釈を周囲の累積階層と結ぶため、同じ基礎的な所属の事実を、対象言語の論理式と外側の構成の両方に用いることができます。

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

## 環境の塔を集合として構成する

この解釈を固定した上で、まずアリティで添字づけられたすべての環境集合を一つの集合に集めます。

塔のモジュールは、環境が値を取る台 `W` を固定します。その第 `n` 項目は、構成可能な数項 `n` と、長さ `n` のすべての環境の集合との、符号化された順序対です。第一成分が長さを記録し、第二成分がちょうどその長さのすべての環境を集めます。

```agda
module Tower (W : S) where
  entry : ℕ → S
  entry n = prʟ (numeralL n) (envSet W n)
```

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

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

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

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

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

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

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

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

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

```agda
  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
```

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

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

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

```agda
          , ( 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 ))) ∣₁ ∣₁ ∣₁ )
```

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

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

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

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

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

```agda
    Goal = ∥ Σ[ n ∈ ℕ ] (fst x ≡ pr (# n) (fst (envSet W n))) ∥₁
```

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

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

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

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

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

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

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

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

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

```agda
          byK : Σ[ k ∈ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] (fst n ≡ fst (numeralL (lower k))) → 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` の内部の外延性が、この二つの方向を、底の集合の等式に変えます。

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

## 環境の塔の有界な仕様

空性の述語は、集合がまったく要素をもたないことを、その要素の上の有界の全称で言います。

```agda
emptyAll : ∀ {m} → Fin m → Formula S m
emptyAll x = ∀̇∈ (var x) ⊥̇
```

空集合の単元の節には二つの連言支があります。その集合が空の要素を一つ含むことと、そのすべての要素が空であることです。両方が要ります。最初のものは存在の条項であり、これがなければ、この述語は空集合自身についても成り立ってしまいます。

```agda
sglEmpty : ∀ {m} → Fin m → Formula S m
sglEmpty F = ∃̇∈ (var F) (emptyAll i0) ∧̇ ∀̇∈ (var F) (emptyAll i0)
```

cons 像の節は、集合の等しさに必要な二方向の包含を与えます。候補となる後続集合の各要素は、ある台の要素をある前段の環境に cons して得られるものでなければなりません。逆に、各前段の環境と各台の要素に対して、対応する cons 拡張が後続集合に存在しなければなりません。両条件を合わせると、後続集合はそれらの cons 拡張だけをちょうど含みます。

```agda
consImage : ∀ {m} → Fin m → Fin m → Fin m → Formula S m
consImage F' F w =
    ∀̇∈ (var F') (∃̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F)) (consAtL i2 i1 i0)))
  ∧̇ ∀̇∈ (var F) (∀̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F')) (consAtL i0 i1 i2)))
```

現在の項目をアリティと環境集合に分解した後、この二つの本体が隣接する一段を記述します。`upBody` は、新しいアリティが現在のアリティの後続であり、新しい環境集合が現在の環境集合の cons 像であることを述べます。`downBody` は役割を逆にし、現在のアリティが前段のアリティの後続であり、現在の環境集合が前段の環境集合の cons 像であることを述べます。

```agda
private
  upBody downBody : ∀ {m} → Fin m → Formula S (8 + m)
  upBody w = sucAtL i5 i1 ∧̇ consImage i0 i4 (sh 8 w)
  downBody w = sucAtL i1 i5 ∧̇ consImage i4 i0 (sh 8 w)
```

上向きの節は、塔の上で存在量化されます。塔のある項目が上向きの本体を満たすのです。

```agda
  towerUp : ∀ {m} → Fin m → Fin m → Formula S (4 + m)
  towerUp E w = ∃̇∈ (var (sh 4 E)) (bothEx i0 (upBody w))
```

下向きの節は選言です。その項目が、空の環境集合をもつ基底の項目と等しいか、あるいは、塔のある項目が、その cons の像が現在の項目である先行者であるかのどちらかです。これが、後の所属帰納の読みを支えます。

```agda
  towerDown : ∀ {m} → Fin m → Fin m → Fin m → Formula S (4 + m)
  towerDown E w N0 =
      ((var i1 ≐ var (sh 4 N0)) ∧̇ sglEmpty i0)
    ∨̇ ∃̇∈ (var (sh 4 E)) (bothEx i0 (downBody w))
```

完全な論理式は、符号化された順序対の項目について三つの有界な条件を連言します。基底の対が `E` に存在すること、`E` のうち順序対のインターフェースを通して読まれる各要素に上向きの後続があること、そしてそのような各対が基底の対であるか前段をもつことです。したがって、`towerAt` が制御するのは、後の読み取りで用いる符号化された順序対の項目です。それだけでは `E` の任意の非順序対要素を排除せず、本章は、この論理式を満たす任意の `E` が構成した `Tower.tower W` と等しいことも導きません。

```agda
towerAt : ∀ {m} → Fin m → Fin m → Fin m → Formula S m
towerAt E w N0 =
    ∃̇∈ (var E) (sndEx i0 (sh 1 N0) (sglEmpty i0))
  ∧̇ ( ∀̇∈ (var E) (bothAll i0 (towerUp E w))
    ∧̇ ∀̇∈ (var E) (bothAll i0 (towerDown E w N0)) )
```

Δ₀ の証拠は検査によって産み出されます。それは、すべての量化子が有界であることだけを証明します。論理式の意味論的な正しさは、後の読みの補題が別に確立するのであって、この証拠によるものではありません。

```agda
Δ₀-towerAt : ∀ {m} (E w N0 : Fin m) → Δ₀ (towerAt E w N0)
Δ₀-towerAt E w N0 = checkΔ₀ (towerAt E w N0) tt
```

## 零アリティと後続アリティの環境集合

事実のモジュールは台 `W` を固定し、長さゼロと後続の長さの環境についての実際の再帰の事実を集めます。

```agda
module EnvFacts (W : S) where
  private
    ι : ⟪ fst W ⟫ → V ℓ
    ι = ⟪ fst W ⟫↪
```

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

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

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

```agda
    g0 : Ix W 0
    g0 ()
```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
  env-split : {k : ℕ} (g' : Ix W (suc k))
            → fst (envS W g') ≡ 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 関数の符号化グラフと同定する等式が単に存在します。

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

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

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

## 後続環境の構成を読む

cons の像の読み手は、候補の後続の集合 `F'`、候補の基底の集合 `F`、アルファベットの枠 `w`、そして環境をパラメータとし、アルファベットの枠を作業集合と揃える等式を伴います。

```agda
module ConsImageRead {m : ℕ} (F' F w : Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) where
  open EnvFacts W
  private
    ι : ⟪ fst W ⟫ → V ℓ
```

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

```agda
    ι = ⟪ fst W ⟫↪
```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
            (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 → ⟨ fst (envS W g) ∈ u ⟩) (sym qF) (envSet-in W g))
            (xS q) (subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q))) })
```

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

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

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

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

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

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

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

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

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

```agda
            xS = ι q , isL-trans {x = fst W} {y = ι q} (ι∈' q) (snd W)
        in xS , ( subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q)
              , ∣ envS W g , ( subst (λ u → ⟨ fst (envS W g) ∈ 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 → ⟨ fst e' ∈ u ⟩) qF' he'))
```

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

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

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

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

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

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

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

数項は構成可能な要素として提示されます。有限の順序数と、その構成可能性の証明です。

```agda
nn : ℕ → S
nn k = # k , numL k
```

## 環境の塔の仕様を読む

一つの空集合のモジュールは、候補の集合の枠と環境をパラメータとします。

```agda
module SglEmpty (W : S) {m : ℕ} (F : Fin m) (γ : S ^ m) where
  open EnvFacts W
```

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

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

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

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

```agda
    none z k y hy = Empty.rec* (k (down z y hy) hy)
```

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

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

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

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

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

```agda
          e∈ })
      hex
```

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

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

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

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

環境の塔の読み手は、候補の塔のスロット `E`、パラメータ集合のスロット `w`、ゼロの数項のスロット `N0`、および解釈環境を固定します。その仮定は、`w` を作業集合 `W` と同定し、`N0` を `# 0` と同定し、`towerAt E w N0` の充足を与えます。以下の二つの読みは、ちょうどこれらの同一視に相対的です。

```agda
module TowerRead {m : ℕ} (E w N0 : Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qN0 : fst (lookup N0 γ) ≡ # 0)
  (h : ⟨ γ ⊨ towerAt E w N0 ⟩) where
  private
    Ev = fst (lookup E γ)
```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
                        , ConsImageRead.consImage-out i4 i0 (sh 8 w) δ' W qw k qF' hci ) })
              (IH (fst n') 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` によって第一成分も同定されます。得られた順序対の等式に沿って移送すれば、標準的な零番目の項目が得られます。

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

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

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

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

```agda
    (λ { (p' , (p'∈ , hb)) → PT.rec (snd (pr (# (suc k)) (fst (envSet W (suc k))) ∈ Ev))
      (λ { (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)` に同定されるので、得られた符号化順序対の等式に沿って移送すれば、標準的な後続項目の所属が証明されます。

```agda
                             (ConsImageRead.consImage-out i0 i4 (sh 8 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` として提示します。そのコンテナが二つの成分を有界量化に公開し、四つの枠からなる環境が、現在の環境集合、数項、コンテナ、塔の項目を順に記録します。

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

塔を保持するモジュールは、候補の塔が、基礎の集合の等式によって実際の塔と同一視されていると仮定します。台と数項の等式に加えてです。すべての結論は、これらの同定に相対的です。

```agda
module TowerHolds {m : ℕ} (E w N0 : Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qE : fst (lookup E γ) ≡ fst (Tower.tower W))
  (qN0 : fst (lookup N0 γ) ≡ # 0) where
  private
    Ev = fst (lookup E γ)
```

すべての正準な項目は、候補の塔に属します。実際の塔の内向きの読み出しを、同定の等式に沿って運ぶことによるものです。

```agda
    entry∈ : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩
    entry∈ k = subst (λ u → ⟨ pr (# k) (fst (envSet W k)) ∈ u ⟩) (sym qE) (Tower.tower-in′ W k)
```

それぞれの正準な項目は、候補の塔の中での所属を下降して、台の要素として提示されます。

```agda
    entryS : (k : ℕ) → S
    entryS k = down (lookup E γ) (pr (# k) (fst (envSet W k))) (entry∈ k)
```

候補の塔のすべての要素は、正準な項目として読まれます。所属を実際の塔の中へ運び、塔の外向きの読み出しを適用することによるものです。

```agda
    read : (p : S) → ⟨ fst p ∈ Ev ⟩ → ∥ Σ[ k ∈ ℕ ] (fst p ≡ pr (# k) (fst (envSet W k))) ∥₁
    read p p∈ = Tower.tower-out W p (subst (λ u → ⟨ fst p ∈ u ⟩) qE p∈)
```

塔を保持する結論は、三つの条項の組です。基底の条項、上向きの閉じの条項、そして下向きの分解の条項です。基底の条項は、零番目の正準な項目とその所属を提示することで証明されます。

```agda
  holds : ⟨ γ ⊨ towerAt E w N0 ⟩
  holds = hbase , (hup , hdown)
    where
    hbase : ⟨ γ ⊨ ∃̇∈ (var E) (sndEx i0 (sh 1 N0) (sglEmpty i0)) ⟩
    hbase = ∣ entryS 0 , ( entry∈ 0
```

零番目の項目は、その数項の等式と所属と、提示された環境に適用した一つの空集合の条項の内向きの読み出しで満たされます。数項の等式は、候補の零の数項の枠から運ばれます。

```agda
      , fillSnd i0 (entryS 0 ∷ γ) (lookup N0 γ) (envSet W 0)
          (cong (λ a → pr a (fst (envSet W 0))) (sym qN0))
          (sglEmpty i0)
          (SglEmpty.sglEmpty-in W i0
            (envSet W 0 ∷ container (lookup i0 (entryS 0 ∷ γ)) (lookup N0 γ) (envSet W 0)
```

基底の節はこれで完成します。その証人は正準な項目 `entryS 0` であり、これが `E` に属することは、`E` と構成済みの塔との同一視から得られます。等式 `qN0` は第一成分を指定されたゼロの数項のスロットに揃え、`SglEmpty.sglEmpty-in` は第二成分を空環境だけからなる一元集合と同定します。したがって、必要な基底の項目が命題的切り詰めのもとで存在します。

```agda
               (cong (λ a → pr a (fst (envSet W 0))) (sym qN0)) .fst ∷ entryS 0 ∷ γ) refl)
          (sh 1 N0) refl ) ∣₁
```

上向き閉包を示すため、`E` の項目 `p` と、`bothAll-in` に渡される任意の符号化順序対表示 `p = (n,F)` を固定します。読み補題 `read p p∈` は、ある `k` について `p` が正準な項目 `(# k, envSet W k)` であることを、命題的切り詰めのもとで述べます。そこで符号化順序対の単射性を使うと、`n` は `# k` と、`F` は `envSet W k` とそれぞれ同定されます。したがって、この議論が使うのは、`towerAt` が制御する符号化順序対のインターフェースに限られます。

```agda
    hup : (p : S) → ⟨ fst p ∈ Ev ⟩ → ⟨ (p ∷ γ) ⊨ bothAll i0 (towerUp E w) ⟩
    hup p p∈ = bothAll-in i0 (towerUp E w) (p ∷ γ) (λ n F s s∈ n∈ F∈ e →
      PT.rec (snd ((F ∷ n ∷ s ∷ p ∷ γ) ⊨ towerUp E w))
        (λ { (k , qp) →
          let q = pr-inj (sym e ∙ qp)
```

次の正準な項目は、`entryS (suc k)` が `E` に属するという証明から得られます。環境 `δ1` は、この項目と現在の項目の成分 `F`、`n` をまとめて記録します。続いて `container` が、新しい順序対の数項成分と環境集合成分を論理式から参照するための有界な容器を与えます。さらに `δ2` へ拡張すると、正準な後続数項と `envSet W (suc k)` が `upBody` の要求するスロットに置かれます。

```agda
              δ1 = entryS (suc k) ∷ F ∷ n ∷ s ∷ p ∷ γ
              c' = container (lookup i0 δ1) (nn (suc k)) (envSet W (suc k)) refl
              δ2 = envSet W (suc k) ∷ nn (suc k) ∷ c' .fst ∷ δ1
          in ∣ entryS (suc k) , ( entry∈ (suc k)
             , fillBoth i0 δ1 (nn (suc k)) (envSet W (suc k)) refl (upBody w)
```

ここで `upBody` の二つの連言は、それぞれ二つの後続段階を表します。`sucAtL` の導入補題は第一成分の等式を `sucV` によって運び、`# (suc k)` と新しい数項のスロットを結びます。一方、`ConsImageRead.consImage-in` は第二成分の等式、同一視 `w = W`、および `consAtL` の妥当性を用いて、`envSet W (suc k)` が `envSet W k` の cons 像にほかならないことを示します。これらの証明から後続項目の切り詰められた証人が得られ、`read` の切り詰められた結果をこの充足命題へ除去することで、すべての項目について上向き閉包が成立します。

```agda
                 ( suc-in i5 i1 δ2 (cong sucV (sym (q .fst)))
                 , ConsImageRead.consImage-in i0 i4 (sh 8 w) δ2 W qw k (q .snd) refl ) ) ∣₁ })
        (read p p∈))
```

下向き分解も同じように始まります。項目 `p` とその任意の符号化順序対表示 `p = (n,F)` を固定し、`read` は命題的切り詰めが許す範囲でだけ使います。得られる証人は、`p = (# k, envSet W k)` を満たすある自然数 `k` を与えます。この証人の `k` をパターン照合すると、`k = 0` と `k = suc j` に分かれます。これらがちょうど `towerDown` の二つの選言です。

```agda
    hdown : (p : S) → ⟨ fst p ∈ Ev ⟩ → ⟨ (p ∷ γ) ⊨ bothAll i0 (towerDown E w N0) ⟩
    hdown p p∈ = bothAll-in i0 (towerDown E w N0) (p ∷ γ) (λ n F s s∈ n∈ F∈ e →
      PT.rec (snd ((F ∷ n ∷ s ∷ p ∷ γ) ⊨ towerDown E w N0))
        (λ { (zero , qp) →
          let q = pr-inj (sym e ∙ qp)
```

`k` がゼロなら、符号化順序対の単射性によって `n` は `# 0` と、`F` は `envSet W 0` とそれぞれ同定されます。第一の等式を `qN0` と合成すると、記録された数項が指定されたゼロの数項であることが分かり、`SglEmpty.sglEmpty-in` は第二の等式を空環境だけからなる一元集合という条件に変えます。これで左の選言が得られます。`k = suc j` なら、同じ単射性から先行する添字とその環境集合が得られ、続く環境が右の選言の証人を用意します。

```agda
          in ∣ inl (q .fst ∙ sym qN0 , SglEmpty.sglEmpty-in W i0 (F ∷ n ∷ s ∷ p ∷ γ) (q .snd)) ∣₁
           ; (suc j , qp) →
          let q = pr-inj (sym e ∙ qp)
              δ1 = entryS j ∷ F ∷ n ∷ s ∷ p ∷ γ
              c' = container (lookup i0 δ1) (nn j) (envSet W j) refl
```

後続の場合、`entryS j` が `E` に属する正準な先行項目を与えます。`sucAtL` の導入補題は第一成分の等式を用いて、現在の数項が先行する数項の後続であることを示します。次に `ConsImageRead.consImage-in` が、`w = W` と第二成分の等式を用いて、現在の環境集合が先行する環境集合の cons 像であることを示します。この先行項目と二つの事実をまとめると、右の選言が要求する切り詰められた証人が得られます。

```agda
              δ2 = envSet W j ∷ nn j ∷ c' .fst ∷ δ1
          in ∣ inr ∣ entryS j , ( entry∈ j
             , fillBoth i0 δ1 (nn j) (envSet W j) refl (downBody w)
                 ( suc-in i1 i5 δ2 (q .fst)
                 , ConsImageRead.consImage-in i4 i0 (sh 8 w) δ2 W qw j refl (q .snd) ) ) ∣₁ ∣₁ })
```

`read` の切り詰められた結果を充足命題へ除去すると、実際の塔のすべての要素について下向き分解が完成します。基底と上向き閉包の条項を合わせれば、`E`、`w`、`N0` がそれぞれ `Tower.tower W`、`W`、`# 0` と同定されるとき、`towerAt E w N0` が充足されます。この結論は、論理式が符号化順序対のインターフェースだけを制御するという境界を保ったまま、実際の塔が有界記述を満たすことを示します。

```agda
        (read p p∈))
```

## まとめ

環境の塔には、後で必要となる二つの形がそろいました。一つは、要素がちょうど標準的な順序対 `(# n, envSet W n)` である実際の構成可能集合です。もう一つは、隣り合うアリティごとに、その符号化順序対の項目を読み取り、生成する Δ₀ 論理式です。二つの向きでは異なる帰納法を使います。項目を読むときは所属帰納によって無限降下を排除し、標準項目をすべて生成するときは自然数に関する通常の帰納法を使います。復元されたアリティと分解はつねに命題的切り詰めのもとにあり、この論理式は、任意の候補集合に含まれうる非順序対の要素について何も主張しません。