累積階層の内部での符号化

この章を読むか、読書案内と依存マップで別のルートを選べます。

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

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

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

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

open import Base.Prelude

module V.Coding {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

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

import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl )

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

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

import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
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 hPropStructure 𝒮ᵥ

数項は互いに異なる

最初の字母は数項写像であり、その単射性は 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 zero    m<0    = Empty.rec (¬-<-zero m<0)
#mono m (suc n) m<sucn = Sum.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 = Empty.rec (∈-irrefl (# n)
      (subst (λ z → ⟨ z ∈ˢ (# n) ⟩) #m≡#n (#mono m n m<n)))

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

... | gt n<m = Empty.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 = PT.rec (setIsSet a c)
    (Sum.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 = PT.rec (setIsSet d b)
    (Sum.rec
      (λ e → singl≡pair (sym e) .snd ∙ a≡b)
      (λ e → PT.rec (setIsSet d b)
        (Sum.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 = PT.rec (setIsSet b d)
    (Sum.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 → PT.rec (setIsSet b d)
        (Sum.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 関係でそれらについて推論できます。