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

対話型目次 · 依存グラフ

この章は固定された宇宙レベル ℓ で述べられる。階層の構造 𝒮ᵥ が符号の載る台であり、その所属関係こそ分析の対象である。最終的な符号化インスタンスは、一つ上のレベル hProp (ℓ-suc ℓ) の真理値を使う。

module V.Coding {ℓ : Level} where

FOL.Coding の一般的な符号化構成が要求するのは、台の上の 2 つの単射操作、すなわち単射な対の操作と自然数からの単射写像だけである。累積階層の上の構文を符号化するには、この 2 つを集合のうちに見つけなければならず、階層自身がそれを供給する。自然数には von Neumann 数項がそのまま使える。各数項は自分の後続の内にあるので、小さい数項は大きい数項に属し、どの集合も自分自身には属しない。したがって、自然数の三分律で比較した異なる添字は異なる集合に写る。対には Kuratowski 符号化が使える。a と b の対とは、一元集合 ⁅ a ⁆s と非順序対 ⁅ a , b ⁆ を元として持つ集合であり、第 1 成分は共通の元として、第 2 成分は (一致しうる) もう一方の元として復元できる。

どちらの議論にも、型理論からの 1 つの制約が関わる。階層の集合における小さい所属は命題の切り詰めを持つので、それに関する場合分けは命題へしか消去できない。V は h-集合なので V の等式は命題的であり、その等式から作られるパス命題が、以下の推論がまさに必要とするターゲットである。この規律のもとでは、すべてのステップが命題に値を取り、切り詰めから証拠を取り出すことは一度もない。

数項の議論は、階層の後続に関する 2 つの所属事実に依存する。任意の集合は自分自身の後続に属し、集合の元はその後続にも属するというものである。数項に適用すると、第 1 の事実は # n ∈ # (suc n) を、第 2 の事実は # n の元が # (suc n) にも残ることを述べる。自然数の順序がどちらの数項が小さいかを決め、三分律の比較 m ≟ n が単射性証明が分ける 3 つの場合を与える。

open import Cubical.Data.Nat.Order using ( _<_; <-split; ¬-<-zero; _≟_; lt; eq; gt )

この消去制限を正確に述べる。小さい所属の主張 ⟨ x ∈ₛ s ⟩ は切り詰めによって命題なので、仮定が所属の切り詰められた選言を与えるとき、消去の行き先は命題でなければならない。V は h-集合であり (setIsSet が証明する)、階層の集合の間のパス型 x ≡ y は命題的である。したがって以下のすべての場合分けはそのような等式パスへ消去できる。

open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )

Kuratowski 符号が必要とする 2 つの集合の構成には、所属の分類が付いている。非順序対 ⁅ a , b ⁆ については、分類 pairing-ax は、切り詰められた意味で x ≡ a または x ≡ b のときに限り x が属することを述べる。一元集合 ⁅ a ⁆s は一元集合パッケージを通して同様の分類を持ち、SetPackage.classification がこれらのレコードを取り出す。したがって、以下の符号に関するすべての議論は、入れ子の中括弧を展開するのではなく、所属の推論として述べられる。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)

数項 # n は #_ と書かれ、階層の中で自然数 n を表す von Neumann 順序数である。2 つの字母が揃えば、hProp (ℓ-suc ℓ) 上の直接の演算と構造 𝒮ᵥ が、章末の符号化インスタンスが符号化された構文を解釈する場になる。この章の単射性証明は、前述の後続の事実と分類だけを使う。

open InfinitySet using ( #_ )

open hPropView 𝒮ᵥ

数項は互いに異なる

最初の字母は数項写像であり、その単射性は 2 つの主張に分かれる。単調性は、小さい数項が大きい数項に属すと言う。帰納は大きいほうの添字に対して行い、各ステップが構文的な後続になるようにして、添字の算術を一切現れさせない。ステップの場合は自然数の三分律によって「真に小さい添字か等しい添字か」に分かれ、それぞれ後続の所属事実が解決する。基底の場合は空虚である。すると単射性が従う。異なる添字の符号が一致すれば、単調性がある数項をそれ自身の内に置くことになり、所属の反射なし性がこれを禁じる。

足場となる #⊆suc は、# n の任意の元が次の数項の元でもあることを述べる。これは「集合の元はその後続に属する」という後続の事実そのものである。#mono の基底の場合は証明すべきことがない。ゼロより真に小さい添字は存在せず、仮定 m < 0 はそのまま反証される。

#⊆suc : (n : ℕ) {x : S} → ⟨ x ∈ˢ (# n) ⟩ → ⟨ x ∈ˢ (# (suc n)) ⟩
#⊆suc n {x} = ∈sucV-inl {A = # n} {x = x}

#mono : (m n : ℕ) → m < n → ⟨ (# m) ∈ˢ (# n) ⟩
#mono m 0    m<0    = ⊥₀-rec (¬-<-zero m<0)
#mono m (suc n) m<sucn = ⊎-rec

後続のステップでは、<-split は m < suc n が m < n か m ≡ n に分かれると言うだけである。第 1 の枝では帰納仮定が # m ∈ # n を与え、#⊆suc がそれを後続へ持ち上げる。第 2 の枝では 2 つの数項が一致しており、集合は自分自身の後続に属するので、m ≡ n の逆向きの輸送によって所属 # n ∈ # (suc n) が求めるものに変わる。

  (λ m<n → #⊆suc n (#mono m n m<n))
  (λ m≡n → subst (λ M → ⟨ (# M) ∈ˢ (# (suc n)) ⟩) (sym m≡n) (self∈sucV (# n)))
  (<-split m<sucn)

単射性は添字の三分律から従う。添字が等しければそれが結論である。m < n なら単調性から # m ∈ # n が得られ、仮定の等式 # m ≡ # n がこの所属を # n ∈ # n へ輸送するが、所属の反射なし性がこれを禁じる。残りの n < m の場合は鏡像で、輸送は逆向きに行われる。

真に小さい場合が示唆的である。所属 # m ∈ # n は数項 # m について述べているが、# m ≡ # n に沿ってその型を書き換えると、その集合は至る所 # n に置き換えられ、# n ∈ # n の要素が得られる。所属の反射なし性はこの要素を空型の元へと送るので、この場合は生じえない。

#-inj : (m n : ℕ) → # m ≡ # n → m ≡ n
#-inj m n #m≡#n with m ≟ n
... | eq m≡n = m≡n
... | lt m<n = ⊥₀-rec (∈-irrefl (# n)
      (subst (λ z → ⟨ z ∈ˢ (# n) ⟩) #m≡#n (#mono m n m<n)))

大きい場合は m と n の役割を入れ替えただけでまったく同じである。単調性が # n を # m の内に置き、等式が逆向きに輸送し、# m の反射なし性がこれを反証する。変種 #-inj′ は同じ主張を添字を暗黙にした形でまとめたもので、符号化インターフェースが消費するのはこの形である。

... | gt n<m = ⊥₀-rec (∈-irrefl (# m)
      (subst (λ z → ⟨ z ∈ˢ (# m) ⟩) (sym #m≡#n) (#mono n m n<m)))

#-inj′ : ∀ {m n} → # m ≡ # n → m ≡ n
#-inj′ {m} {n} = #-inj m n

Kuratowski 対

2 番目の単射な字母は Kuratowski 対である。a と b の符号は、一元集合 ⁅ a ⁆s と非順序対 ⁅ a , b ⁆ を元として持つ集合である。順序を記録する外側の順序対と、順序を記録しない内側の非順序対を区別してほしい。単射性とは両成分が符号から復元できることであり、この復元は完全に分類仕様によって進められる。一元集合への所属はその唯一の元に等しいことであり、非順序対への所属は切り詰められた意味で 2 つの成分のどちらかに等しいことにすぎない。

一元集合の分類は両方向に一度だけ名前を与えられる。∈singl は ⁅ a ⁆s の元が a と等しいことを、singl∈ は等しければ属することを述べる。どちらも一元集合パッケージの同じ分類レコードの射影である。

private
  ∈singl : {a x : S} → ⟨ x ∈ₛ ⁅ a ⁆s ⟩ → x ≡ a
  ∈singl {a} {x} = SetPackage.classification (SingletonPackage a) x .fst

  singl∈ : {a x : S} → x ≡ a → ⟨ x ∈ₛ ⁅ a ⁆s ⟩
  singl∈ {a} {x} = SetPackage.classification (SingletonPackage a) x .snd

非順序対については、分類は切り詰められた選言の形を持つ。⁅ a , b ⁆ の元は、切り詰められた意味で a に等しいか b に等しい。2 つの導入補題は左右の選言支を切り詰められた証拠として供給するので、いずれかの等式から何も選ばずに所属を作れる。

  self∈singl : (a : S) → ⟨ a ∈ₛ ⁅ a ⁆s ⟩
  self∈singl a = singl∈ refl

  inl∈⁅,⁆ : {a b x : S} → x ≡ a → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩
  inl∈⁅,⁆ {a} {b} {x} e = pairing-ax a b x .snd ∣ inl e ∣₁

  inr∈⁅,⁆ : {a b x : S} → x ≡ b → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩

一元集合はその元を決定する。⁅ a ⁆s ≡ ⁅ c ⁆s なら、所属 a ∈ ⁅ a ⁆s をこのパスに沿って輸送し、結果を分類すれば、それは c と等しくなければならない。消去はパス命題 a ≡ c へ向かい、V が h-集合なのでこれは許される。

  inr∈⁅,⁆ {a} {b} {x} e = pairing-ax a b x .snd ∣ inr e ∣₁

  mem⁅,⁆ : {a b x : S} → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩ → ∥ (x ≡ a) ⊎ (x ≡ b) ∥₁
  mem⁅,⁆ {a} {b} {x} = pairing-ax a b x .fst

  singl-inj : {a c : S} → ⁅ a ⁆s ≡ ⁅ c ⁆s → a ≡ c
  singl-inj {a} {c} q = ∈singl (subst (λ s → ⟨ a ∈ₛ s ⟩) q (self∈singl a))

一元集合がたまたま非順序対と等しいときは、非順序対の両成分がその一元集合の元へ押し下げられる。各成分は切り詰められた意味でその非順序対に属するので、所属を sym q の向きに輸送して分類すると、その成分から a へのパスが得られる。どちらの消去もパス命題の組 (c ≡ a) × (d ≡ a) をターゲットにする。この退化的な比較こそ、後の対の単射性の難所である。

  singl≡pair : {a c d : S} → ⁅ a ⁆s ≡ ⁅ c , d ⁆ → (c ≡ a) × (d ≡ a)
  singl≡pair {a} {c} {d} q =
      ∈singl (subst (λ s → ⟨ c ∈ₛ s ⟩) (sym q) (inl∈⁅,⁆ {a = c} {b = d} refl))
    , ∈singl (subst (λ s → ⟨ d ∈ₛ s ⟩) (sym q) (inr∈⁅,⁆ {a = c} {b = d} refl))

対の単射性の証明は、4 つの比較補題から組み上げられる。p : pr a b ≡ pr c d が与えられると、符号の一元集合の部分は両側に属するので、その所属を p に沿って前向きに輸送して分類すれば、切り詰められた意味で ⁅ a ⁆s ≡ ⁅ c ⁆s か ⁅ a ⁆s ≡ ⁅ c , d ⁆ が得られる。第 1 の選言支は直ちに a ≡ c を与え、第 2 の選言支は singl≡pair の逆向きを通して与える。非順序対の部分はより難しく、所属だけでは第 2 成分が決まらないことがある。符号が潰れるとき、⁅ a , b ⁆ は左か右で一元集合と一致するが、どちら側と一致したかを知るだけでは足りない。そこで 2 つの切り詰められた記録を取っておく。1 つは ⁅ a , b ⁆ が pr a b に属することから p に沿って前向きに輸送したもの、もう 1 つは ⁅ c , d ⁆ が pr c d に属することから p の逆向きに輸送したものである。後ろ向きの記録が、退化した枝に欠ける情報をまさに補う。一時的な仮定 a ≡ b のもと、すなわち符号全体が一元集合の一元集合に潰れる場合には、復元した a ≡ b を d ≡ b に変換する。この証明での切り詰められた選言の消去はすべて、h-集合 V のパスからできる命題をターゲットにするので、証拠が選び出されることはない。

符号 pr a b は、一元集合 ⁅ a ⁆s と非順序対 ⁅ a , b ⁆ を 2 つの元として持つ非順序対である。外側の式が順序を記録する Kuratowski 符号であり、その 2 番目の材料である内側の ⁅ a , b ⁆ と混同しないでほしい。内側は順序を記録せず、順序を記録するのは符号全体である。単射性とは、符号の等式 pr a b ≡ pr c d が両方の入力を決定する、つまりパス a ≡ c と b ≡ d を与えるという主張である。

pr : S → S → S
pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆

pr-inj : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d)
pr-inj {a} {b} {c} {d} p = a≡c , b≡d
  where

第 1 成分。一元集合の部分 ⁅ a ⁆s は右の選言支によって pr a b に属するので、この所属を p に沿って輸送して分類すると、切り詰められた意味で ⁅ a ⁆s ≡ ⁅ c ⁆s か ⁅ a ⁆s ≡ ⁅ c , d ⁆ が得られる (これが H₁ である)。第 1 の選言支では singl-inj が直接 a ≡ c を与える。第 2 の選言支では比較 singl≡pair が c ≡ a を強制し、その逆向きが求めるものである。切り詰められた選言はパス命題 a ≡ c へ消去され、V が h-集合なのでこれは許される。

  H₁ : ∥ (⁅ a ⁆s ≡ ⁅ c ⁆s) ⊎ (⁅ a ⁆s ≡ ⁅ c , d ⁆) ∥₁
  H₁ = mem⁅,⁆ (subst (λ s → ⟨ ⁅ a ⁆s ∈ₛ s ⟩) p (inl∈⁅,⁆ {b = ⁅ a , b ⁆} refl))

  a≡c : a ≡ c
  a≡c = rec₁ (setIsSet a c)
    (⊎-rec singl-inj (λ e → sym (singl≡pair e .fst))) H₁

第 2 成分。ここでは切り詰められた 2 つの記録を集める。H₂ は非順序対の部分が pr a b に属することから来ており、p に沿って前向きに輸送すると、切り詰められた意味で ⁅ a , b ⁆ が ⁅ c ⁆s か ⁅ c , d ⁆ に等しいことが分かる。K は同じ議論を逆向きに実行し、⁅ c , d ⁆ が pr c d に属することから sym p に沿って輸送して、切り詰められた意味で ⁅ c , d ⁆ が ⁅ a ⁆s か ⁅ a , b ⁆ に等しいことを得る。両方が必要なのは、後述の退化した場合では、1 つの記録だけでは残る隙間をもう 1 つの記録しか埋められないからである。

  H₂ : ∥ (⁅ a , b ⁆ ≡ ⁅ c ⁆s) ⊎ (⁅ a , b ⁆ ≡ ⁅ c , d ⁆) ∥₁
  H₂ = mem⁅,⁆ (subst (λ s → ⟨ ⁅ a , b ⁆ ∈ₛ s ⟩) p (inr∈⁅,⁆ {a = ⁅ a ⁆s} refl))

  K : ∥ (⁅ c , d ⁆ ≡ ⁅ a ⁆s) ⊎ (⁅ c , d ⁆ ≡ ⁅ a , b ⁆) ∥₁
  K = mem⁅,⁆ (subst (λ s → ⟨ ⁅ c , d ⁆ ∈ₛ s ⟩) (sym p) (inr∈⁅,⁆ {a = ⁅ c ⁆s} refl))

  d≡b-from-K : a ≡ b → d ≡ b

補助補題 d≡b-from-K は、一時的な仮定 a ≡ b のもとで退化した状況を処理する。すなわち符号の 2 つの材料が一致し、pr a b が非順序対 ⁅ ⁅ a ⁆s , ⁅ a ⁆s ⁆ に退化する場合である。K を読むと、⁅ c , d ⁆ が一元集合 ⁅ a ⁆s と等しいなら、その分類から d ≡ a、したがって d ≡ b が得られる。⁅ a , b ⁆ と等しいなら、d は切り詰められた意味で a か b に等しく、どちらの選択肢も合成して d ≡ b になる。すべての消去はパス命題 d ≡ b に着地する。

  d≡b-from-K a≡b = rec₁ (setIsSet d b)
    (⊎-rec
      (λ e → singl≡pair (sym e) .snd ∙ a≡b)
      (λ e → rec₁ (setIsSet d b)
        (⊎-rec (λ d≡a → d≡a ∙ a≡b) (λ d≡b → d≡b))

b ≡ d の主議論は H₂ を通って進む。第 1 の選言支では、内側の非順序対 ⁅ a , b ⁆ が一元集合 ⁅ c ⁆s と等しく、比較 singl≡pair を逆向きに読むと b ≡ c が得られる。a ≡ c と b ≡ c の逆向きの合成からパス a ≡ b が従い、これは補助補題が消費する仮定そのものである。補助補題は次に d ≡ b を与え、その逆向きが目標である。ここで後ろ向きの記録 K が効く。補助補題は K から述べられているので、前向きの分類だけではこの場合に届かない。

        (mem⁅,⁆ (subst (λ s → ⟨ d ∈ₛ s ⟩) e (inr∈⁅,⁆ {a = c} refl)))))
    K

  b≡d : b ≡ d
  b≡d = rec₁ (setIsSet b d)
    (⊎-rec

H₂ の第 2 の選言支では、内側の 2 つの非順序対が一致する。⁅ a , b ⁆ ≡ ⁅ c , d ⁆。すると b は切り詰められた意味で ⁅ c , d ⁆ に属するので、b の所属を分類して b ≡ c か b ≡ d が得られる。後者はそのまま目標で、前者は前に示したのと同じ合成と補助補題を経て後者に帰着する。

      (λ e → let b≡c = singl≡pair (sym e) .snd
             in sym (d≡b-from-K (a≡c ∙ sym b≡c)))
      (λ e → rec₁ (setIsSet b d)
        (⊎-rec
          (λ b≡c → sym (d≡b-from-K (a≡c ∙ sym b≡c)))

2 つの枝が合わさって b ≡ d となり、pr-inj が完結する。Kuratowski 符号の両成分は符号の等式から復元できるということである。どの枝も、切り詰められた選言を h-集合 V のパスからできる命題へ消去したものであり、切り詰めから証拠を選び出した箇所はない。

          (λ b≡d → b≡d))
        (mem⁅,⁆ (subst (λ s → ⟨ b ∈ₛ s ⟩) e (inr∈⁅,⁆ {a = a} refl)))))
    H₂

具体化

2 つの単射な字母がそろったので、FOL.Coding の一般的な符号化構成を階層に適用できる。単射な対の操作と単射な数項写像がその 2 つのパラメータである。得られる VCode は、階層の台の上の項と論理式に対して、それ自身が階層の集合である符号を割り当てる。すべての集合を符号にするのではなく、符号化された構文に対して集合値の符号を与えるものである。

レベルに注意してほしい。VCode はレベル ℓ-suc ℓ で取られる。これは、ZFStructureₕ 𝒮ᵥ の関係が値を取るレベルである。この宇宙の指標は型理論のレベルであって、階層の段階ではない。

インスタンス化では、レベル ℓ-suc ℓ、構造 𝒮ᵥ、そして上で確立した 4 つのデータ、すなわち pr-inj を伴う pr と、#-inj′ を伴う数項写像 #_ を渡す。古典的公理・リサイズ・選択の仮定は一切使われず、このインスタンスは分類仕様と 2 つの単射性証明だけに依存する。

module VCode = FOL.Coding {ℓ-suc ℓ} 𝒮ᵥ pr pr-inj #_ #-inj′

まとめ

一般的な符号化が必要とする 2 つの単射な操作は、もとから階層の中にあった。数項は単射である。#-inj は単調性と所属の反射なし性から、自然数の三分律のもとで従う。Kuratowski 対も単射である。pr-inj は一元集合と非順序対の分類仕様を通して両成分を復元する。したがってインスタンス VCode は、レベル ℓ-suc ℓ で、しかもいかなる古典的仮定もなしに、階層の上への FOL.Coding の構成を供給する。階層の集合上の項と論理式は今や V の集合である符号を持ち、Codes 関係でそれらについて推論できる。