この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

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

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

充足関係の節には、L の内部で、ある基礎集合の上の与えられた長さの環境をちょうどすべて集めた一つの集合が必要である。これまでの章は二つの材料を別々に与えた。要素によってそのような集合を特徴づける論理式 envSetAt と、前章で構成した集合 envSet B m である。ある集合がこの記述を満たすのは、その各要素が集合として、基礎の上の長さ m の環境のグラフであるとき、かつそのときである。本章は、記述と構成済みの集合が一致することを証明する。一致には二つの読み方がある。充足の判断によって記述の集合スロットに置かれた集合は、構成済みの集合とちょうど同じ要素を持ち、また構成済みの集合それ自体が記述を満たすので、自分の基礎と長さを束縛する節は、構成済みのデータでスロットを埋めてから記述を引用できる。

どちらの読み方も、要素から復元された環境という一つの対象の上で行われる。単値性、数項による定義域、基礎への所属、そして数項と基礎の要素からなる対、という四つの内部の節が、ある集合がこのようなグラフであることを述べる。前の章はそこから割り当ての関数を復元し、その集合を関数の正準なグラフと同一視した。本章の各段階は、この復元をいずれかの方向に走らせることと、名指されたスロットの一致する環境の間で環境の節の充足を運ぶ輸送の補題とに帰着する。

本書の常設のオプションは引き続き有効である。本章で唯一用いる非構成的な入力は、下のパラメータ lem として明示される。

基礎語彙は「基礎語彙」の章の配置どおり全体として導入される。排中律はオプションとしてではなくデータとして現れ、本章はこれをパラメータとして受け取る。

モジュールパラメータはレベル ℓ-suc ℓ の排中律の実例で、二つの構造の充足の主張の住むレベルに一致する。これは、この章が引用する環境の集合を構成した章へそのまま渡される。

言語を解釈する構造は二つであり、本章はその間を行き来する。周囲の構造 𝒮ᵥ は階層そのものであり、内側の構造 𝒮ʟ はそれを構成可能な集合のクラス isL に制限したものである。このクラスは推移的であり、isL-trans がそれを記録する。絶対性の機構は、まさにこの組の上で働くために導入される。

二つの論理式とその読み方が本章の仕事を担う。環境の節 envOverAt は、候補のグラフが単値であり、その定義域が指定された定義域スロットの集合とちょうど一致し、値が指定された基礎集合に属し、その二つの集合の要素からなる対だけを含むことを述べ、輸送の補題は、名指されたスロットの一致する環境の間でこの節の充足を運ぶ。外延的な記述 envSetAt は、二つの全称含意の形で、ある集合の要素がちょうどそれらの環境であることを述べ、三つの読み方がこれらの含意をどちらの向きにもほどく。

前の章から来るのは、構成済みの集合 envSet、その二つの所属の補題、正準なグラフの要素 envS、みずからの正準な環境で満たされる環境の節 envOver、そして復元のモジュールである。復元のモジュールは四つの節から環境を読み取り、その集合をその環境のグラフと同一視する。

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_ )

環境の集合への所属からそれを表す環境を復号すると、切り詰められた証人だけが得られる。一方、目標となる充足と所属の主張はいずれも命題である。周囲の数項 # m が長さのスロットを埋める。

open hPropView 𝒮ʟ

内側の構造を開くと、全章で使う充足の記法が固定される。その台の要素、その所属関係、そして L の中で読まれる充足の判断である。

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

絶対性のモジュールは構成可能な集合という推移的クラスの上で実例化され、その内側の充足関係には平易な _⊨_ の名が与えられる。本章が読む論理式はすべて L の上のものであり、それと競う読み方はほかにないからである。

記述から所属関係へ

最初のモジュールは、基礎集合 B、長さ k の環境 γ、その三つのスロット、長さ m、そして二つの等式を固定する。等式は、長さのスロットが m の数項で、基礎のスロットが B で埋められていることを述べる。前提は、γ が集合スロットを Ei に置いた記述を満たすことである。結論は要素の一致である。Ei の指す集合と構成済みの envSet B m は、ちょうど同じ集合を含む。

どちらの方向も、同じ二つの材料の上を走る。復元のモジュールは四つの節から環境を読み取り、その出所の集合をその環境の正準なグラフと同一視し、輸送の補題は、名指されたスロットの一致する環境の間を、まさにそれらの名指しの等式に沿って環境の節の充足を運ぶ。どちらの方向も、記述や構成を証明し直すことはない。

private
  nn : ℕ → S
  nn j = # j , numL j

長さのスロットは数項で埋められ、その数項自身も L の要素でなければならない。補助定義 nn がこれを作る。周囲のフォン・ノイマン数項 # j に、その構成可能性の証明を対にしたものである。

module Ambient (B : S) {k : ℕ} (γ : Vec S k) (Ei di bi : Fin k) (m : ℕ)
  (qd : (lookup di γ) .fst ≡ # m) (qb : (lookup bi γ) .fst ≡ B .fst)
  (hE : ⟨ γ ⊨ envSetAt Ei di bi ⟩) where

モジュールは、この問いの一つの実例のデータを集める。B は基礎集合、γ は長さ k の環境で、三つのスロットに名前が付く。Ei が候補の集合を、di が長さの数項を、bi が基礎を収める。等式 qd と qb は、この二つのスロットが m の数項と B で埋められていることを述べ、hE は、γ が集合スロットを Ei に置いた記述を満たすことを述べる。このデータのもとで、Ei の指す集合と envSet B m が同じ要素をもつことが示される。

into : (z : S) → ⟨ z .fst ∈ (lookup Ei γ) .fst ⟩
     → ⟨ z .fst ∈ (envSet B m) .fst ⟩

最初の方向は、スロットの集合を内側へ読むものである。Ei の指す集合のどんな要素も、構成済みの envSet B m の要素である。

into z hz = subst (λ w → ⟨ w ∈ (envSet B m) .fst ⟩)
  (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))
  (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))

証明は、前の章の復元をこの要素そのものに向けて再利用する。仮定は z が Ei の指す集合に属することを言うので、記述は z で適用できる。復元は z から環境 g を読み取り、その正準なグラフが集合として z 自身であると同定する。構成済みの集合はそのような環境の正準なグラフをすべて含むので、この同定に沿って輸送すれば、要素 z は envSet B m の中に入る。

  where
  ov : ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
  ov = extAt-out Ei (envOverAt zero (suc di) (suc bi)) γ hE z hz

復元には、四つの節が z で成り立つことが要る。記述が与えるのはまさにこれである。要素 z に適用すれば、z で拡張した環境の上の環境の節が得られ、長さと基礎のスロットは新しい項目のぶんだけ後ろへずれる。

outof : (z : S) → ⟨ z .fst ∈ (envSet B m) .fst ⟩
      → ⟨ z .fst ∈ (lookup Ei γ) .fst ⟩

第二の方向は外向きに読むものである。構成済みの envSet B m のどんな要素も、Ei の指す集合の要素である。

outof z hz = rec₁ ((z .fst ∈ (lookup Ei γ) .fst) .snd)
  (λ { (g , eg) →

構成済みの集合への所属は、切り詰められた証人を手渡す。それは環境 g であり、その正準なグラフが z である。目標は所属の主張、つまり命題なので、切り詰めは消去でき、証人を生み出すのは前の章の所属の特徴づけである。

    extAt-in Ei (envOverAt zero (suc di) (suc bi)) γ hE z
      (envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)
        (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
        (sym eg) (sym qd) (sym qb)
        (envOver B g)) })

復元された環境は、みずからの正準な環境、すなわち三つのスロットに B と m の数項とそのグラフが収まった環境で、環境の節を満たす。輸送の補題は、三つの等式に沿ってこの充足を拡張された環境 (z ∷ γ) へ運ぶ。正準なグラフを z と読み、数項を di の項目と読み、B を bi の項目と読むのである。記述はその内向きの含意を通して直ちに適用でき、z が Ei の指す集合に属すると結論される。

  (envSet-out B m z hz)

輸送に渡される環境は、構成済みの集合の所属の特徴づけから来る。この方向の出発点であった要素 z に適用されるのである。

構成した集合が記述を満たすこと

第二のモジュールは一致を逆向きに回し、生み出す方向を問う。構成済みの環境の集合それ自体は、この記述を満たすのであろうか。集合のスロットに置き、他の二つのスロットに m の数項と基礎を置けば、答えは肯定的である。これこそ、自分の基礎と長さを束縛する節が、構成済みのデータでスロットを埋める際に必要とするものである。証明は以前と同じ二つの働きを、今度は記述の要求する順序で行う。構成済みの集合の各要素が要素ごとの節を満たすこと、そしてその節を満たす集合がすべて要素であることが示される。

モジュールは充足に関する前提を一切仮定しない。三つの等式が、集合のスロットに構成済みの集合そのものが、長さのスロットに m の数項が、基礎のスロットに B が収まっていることを述べる。これだけから、γ での記述の全体が証明される。

module AmbientHolds (B : S) {k : ℕ} (γ : Vec S k) (Ei di bi : Fin k) (m : ℕ)
  (qE : (lookup Ei γ) .fst ≡ (envSet B m) .fst)
  (qd : (lookup di γ) .fst ≡ # m) (qb : (lookup bi γ) .fst ≡ B .fst)
  where

三つの等式が前提のすべてである。集合のスロットを構成済みの集合で、長さのスロットを数項で、基礎のスロットを基礎で名指すのは、節が三つのスロットを構成済みのデータで埋めるときに行うことそのものであり、したがってモジュールが証明する記述は、そのような節が消費する形そのものである。

holds : ⟨ γ ⊨ envSetAt Ei di bi ⟩
holds = extAt-in-both Ei (envOverAt zero (suc di) (suc bi)) γ fwd bwd

記述は外延的なものである。Ei の指す集合がちょうどそれらの環境を含むことを述べ、その二つの全称含意を別々に証明してから結ぶ。モジュールの冒頭で予告した形が、ここで埋められる。

  where
  fwd : (z : S) → ⟨ z .fst ∈ (lookup Ei γ) .fst ⟩
      → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩

順方向の含意が生み出す方向である。構成済みの集合の各要素は、拡張された環境の上で要素ごとの節を満たす。

  fwd z hz = rec₁ (((z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi)) .snd)
    (λ { (g , eg) → envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)

所属 hz は、まず等式 qE に沿って構成済みの集合へと指し直され、前の章の所属の補題が切り詰められた環境を手渡す。反対側の目標は充足の判断の一つの節、つまり命題なので、切り詰められた証人を分解できる。

           (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
           (sym eg) (sym qd) (sym qb) (envOver B g) })

復元された環境の環境の節は、読み取りの方向とまったく同じやり方で輸送される。その正準な環境から判断の拡張された環境へ、グラフは要素 z と読み、数項は di の項目と読み、基礎は bi の項目と読まれる。残るのは節そのものであり、順方向の含意が負っているのはこれである。

    (envSet-out B m z (subst (λ w → ⟨ z .fst ∈ w ⟩) qE hz))

輸送に渡される環境は、構成済みの集合の所属の特徴付けから来る。qE が最初の一歩、すなわちその要素を envSet B m の要素として読み直す段階を供給する。

  bwd : (z : S) → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
      → ⟨ z .fst ∈ (lookup Ei γ) .fst ⟩

逆方向の含意は読み取りの方向である。拡張された環境の上で要素ごとの節を満たすものは、すべて Ei の指す集合に属する。

  bwd z h = subst (λ w → ⟨ z .fst ∈ w ⟩) (sym qE)
    (subst (λ w → ⟨ w ∈ (envSet B m) .fst ⟩)
      (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb h))
      (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb h)))

z での節は、復元の入力である。復元された環境の正準なグラフは集合として z と一致し、構成済みの集合はそのグラフを含む。最初の輸送が復元されたグラフを z と読み、所属を envSet B m の中に着地させ、二度目の輸送が qE に沿って逆に走り、envSet B m への所属を Ei の指す集合への所属へ変える。