数項列

宇宙レベル ℓ を固定する。このレベルをパラメータとして保つことで、異なる宇宙を同一視せずに、必要な大きさで構成を具体化できる。

module L.Axioms.Numerals {ℓ : Level} where

本章ではモデル自身の空集合、対、和集合の演算から L 内部の自然数列を構成し、それが周囲のフォン・ノイマン数項へ射影されることを証明する。

数学的な問いはこうである。集合 a のフォン・ノイマン後者は a ∪ {a} であるが、L のモデルは自前の空集合、非順序対、和集合を標準的な実現者として供給する。それぞれ、所属の仕様を満たす集合の可縮な型の中心であり、確定記述の演算子 ℩ によって読み出される。そのような中心は仕様をもつ演算であって計算規則ではない。その定義自身は、基底の集合が周囲の階層が自前の対と和集合から作る集合と同じであるとは言っていない。したがって、この列を階層の数項列と比較する前に、射影方程式の族が必要である。各方程式は、モデルの演算が基底の集合を通して読めば階層の対応する演算である、と述べる。

各射影方程式の議論には固定した形がある。可縮な型の中心を、明示的に作った実現者と比較する。対の場合、その実現者は、二つの基底の集合の単に存在する共通段階 (isL-directed が供給する) に有界な対の構成を適用したものである。可縮性は中心からその実現者へのパスを与え、基底集合への射影関数をそのパスに適用すると、集合の間の等式が得られる。切り詰められたデータの消去が正当なのは、目標が階層の集合の間の等式、すなわち命題だからであり、これは階層の台が h-集合であることに依る。射影方程式が手に入れば、内部の列と階層の列は一歩ずつ一致し、モデルの record が数項列に要求する二つの指定方程式も、階層自身の事実をそれらに沿って輸送して従う。

章全体が構成的である。排中律もサイズ変更も、実現者の型の可縮性を超える選択も用いない。本章が行わないのは、数項を一つの集合へ収集することである。その収集こそ無限公理自身の内容である。

鍵となる概念は一意な実現である。対の仕様は λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b) であり、hasPairL a b は、それを実現する構成可能集合の型 SetOf が可縮であることを証明する。すなわち、標準的な実現者である中心と、中心から他のすべての実現者へのパスがあるのである。和集合も同様に hasUnionL によって仕様が与えられ証明される。可縮性の証明は明示的なデータであって、単なる存在主張ではない。中心と収縮の両方を含み、以下で選ばれるのはこの中心である。これが本章で用いる唯一の形の選択であり、それは可縮性そのものによって供給される。

射影方程式は両側を出会わせる。モデルの側には、hasPairL と hasUnionL とその実現の構成 PairOf と UnionOf、そして内部の空集合 ∅ʟ がある。周囲の側には、階層の非順序対 ⁅ _, _ ⁆ と和集合 ⋃_、後者 sucV、数項 #_ がある。両側を結ぶ入力は isL-directed である。これは、二つの構成可能集合の基底の集合を含む共通の順序数段階を、単に存在するものとして供給する。有界な対の構成が実現者を作るには、まさにそのような段階が必要である。二つの内部の演算は、まず定義されて初めて比較できる。

射影方程式は、周囲の階層の集合の間の等式である。たとえば (pairʟ a b) .fst ≡ ⁅ (λ p → p .fst) a , (λ p → p .fst) b ⁆。この特定の等式の型が命題なのは、階層の台が h-集合だからであり、setIsSet が保証するのはまさにそれである。この命題性ゆえに、切り詰められた段階のデータをそこへ消去できる。任意の等式の型について命題性を主張しているのではない。

open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; ⋃_; module InfinitySet )

コードを読みやすくする約束が二つある。構造 𝒮ʟ は集合論のモデルとして提示された構成可能宇宙であり、そのモデルのパッケージを開くと、SetOf、すなわち台の要素とその実現の仕様の対の型、そして ℩、すなわち可縮な SetOf の型の中心の第一成分を返す演算子が使える。全体を通して、台 S の要素への fst は周囲の階層の基底の集合を取り出す。射影方程式が比較するのはまさにこの基底の集合である。

open InfinitySet using ( sucV; #_ )

open hPropView 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; ℩ )

モデル自身の演算

確定記述の演算子は、実現者の型の可縮性を演算に変える。pairʟ と unionʟ は hasPairL と hasUnionL の中心を選び、後者はそれらを合成する。

以下を支配する区別が一つある。可縮な型から選んだ中心は、仕様をもつ演算であって計算規則ではない。可縮性の証明は、pairʟ a b の基底の集合を階層の対 ⁅ (λ p → p .fst) a , (λ p → p .fst) b ⁆ へ簡約するものではない。実際に与えるのは、中心からすべての実現者へのパスであり、次節の射影方程式は、そのパスに沿って中心を明示的に作った実現者と比較することで得られる。三つの演算はすべて opaque と宣言され、以後の使用はその構成ではなく、仕様と射影方程式を通して読まれる。

演算子 ℩ は可縮性の証明を受け取り、その中心の第一成分、すなわち台 S の要素を返す。これを hasPairL a b と hasUnionL a に適用すれば、構成可能集合の上の二つの関数が得られる。入力は台の要素、つまり構成可能性の証明書とともにまとめられた集合なので、各演算は入力がすでに持つもののほかに引数を必要としない。

opaque
  pairʟ : S → S → S
  pairʟ a b = ℩ (hasPairL a b)

  unionʟ : S → S
  unionʟ a = ℩ (hasUnionL a)

内部の後者は両者を合成する。sucʟ a = unionʟ (pairʟ a (pairʟ a a))。内側の対は a とそれ自身の非順序対である。後で基底の集合に適用される一元集合の法則がこの内側の対を {a} と同一視し、外側の対の二つの項は a とその一元集合になる。したがって、式が a ∪ {a} へ崩れるのはそのためである。ここで扱うのは外側の非順序対とその二つの項であって、順序対やその成分ではない。

  sucʟ : S → S
  sucʟ a = unionʟ (pairʟ a (pairʟ a a))

射影方程式

可縮性により取り出した演算を周囲の階層の非順序対および和集合と同一視し、内部の後者について射影方程式を得る。

可縮な型の中心は、一見すると階層が作るであろう集合ではない。ここで演算は opaque なので、本章では定義を展開せず、射影方程式を通して階層の演算と比較するからである。しかし可縮性が語るのは存在にとどまらず、すべての実現者がまさに中心である、ということである。そこで証明は、手元にある段階のデータから明示的な実現者を作り、それに収縮を適用して中心からその実現者へのパスを得る。各収縮は、目標が階層の集合の間の等式であるような切り詰められたデータの消去の内部で適用される。その目標が命題なのは階層の台が h-集合だからであり、これが消去を正当化する。

主張はまず目標を固定する。取り出した対の基底の集合が、階層が基底の集合たちに作る非順序対と等しいこと。消去 rec₁ が isL-directed の単に存在する共通段階のデータを開くが、これが正当なのは、目標は等式 (pairʟ a b) .fst ≡ ⁅ (λ p → p .fst) a , (λ p → p .fst) b ⁆ であり、setIsSet ((pairʟ a b) .fst) ⁅ (λ p → p .fst) a , (λ p → p .fst) b ⁆ がこの等式の型を命題だと証明することだからである。内部では、届くデータ σ , oσ , fa∈ , fb∈ がちょうど PairOf.mkPair が消費するものであり、mkPair はそこから実現者を構成する。証明書が供給するパスは中心からその実現者へ向かうものであり、逆向きではない。

  pairʟ-fst : (a b : S) → (pairʟ a b) .fst ≡ ⁅ a .fst , b .fst ⁆
  pairʟ-fst a b = rec₁ (setIsSet ((pairʟ a b) .fst) ⁅ a .fst , b .fst ⁆)
    (λ { (σ , (oσ , (fa∈ , fb∈))) →
         cong (λ (e : SetOf (PairOf.Q a b)) → (e .fst) .fst)
           (hasPairL a b .snd (PairOf.mkPair a b σ oσ fa∈ fb∈)) })

最後の一歩は、中心と明示的に構成した実現者を同一視する。収縮 hasPairL a b .snd は任意の実現者に対して、中心からその実現者へ向かうパスを与える。これを mkPair a b σ oσ fa∈ fb∈ に適用すると、型 SetOf (PairOf.Q a b) の中のパスが得られる。この型は台の要素をその実現の仕様とともにまとめたものである。射影関数 λ e → (e .fst) .fst をこのパスに適用することで、台の要素を読み取りつぎにその基底の集合を読み取りる射影が、このパスを基底の集合の間の等式に変え、目標が閉じる。切り詰められた共通段階のデータが消去される先はこの集合の等式だけであり、その命題性は setIsSet が供給する。和集合の場合は、入力が一つ少ないだけの同じ議論である。UnionOf.mkUnion は a .fst を含む一つの段階を必要とするだけで、証明書 a .snd はまさにそのような、単に存在する段階のデータなので、消去はそれを直接消費する。

    (isL-directed (a .fst) (b .fst) (a .snd) (b .snd))

  unionʟ-fst : (a : S) → (unionʟ a) .fst ≡ ⋃ (a .fst)
  unionʟ-fst a = rec₁ (setIsSet ((unionʟ a) .fst) (⋃ (a .fst)))
    (λ { (σ , (oσ , fa∈)) →
         cong (λ (e : SetOf (UnionOf.Q a)) → (e .fst) .fst)

結果を読めば (unionʟ a) .fst ≡ ⋃ (a .fst)、モデルの和集合の演算の基底の集合は、階層が基底の集合に作る和集合である。対の方程式と合わせて、モデルの対と和集合から組み立てた集合は、基底の集合を通して読めば、階層の演算から組み立てた同じ集合になる。射影方程式の用途はまさにここにある。二つの後者の演算を、ひいては二つの数項列を、一歩ずつ比較することである。

           (hasUnionL a .snd (UnionOf.mkUnion a σ oσ fa∈)) })
    (a .snd)

後者の方程式は、射影方程式を合成したものであり、そこに階層自身の {a, a} と {a} の同一視が加わる。外側の和集合を展開し、つぎに外側の対、つぎに内側の対を展開し、最後に重複した一元集合を潰せば、残るのは階層の後者である。

各段階では一つの関数を既存の等式に適用し、入れ子の位置を一つずつ書き換えるだけなので、合成は外から内へ進む。各因子の向きが重要である。対の方程式は取り出した中心から階層の対へ向かうので、周囲の「対の和集合」という関数をその等式に適用することが項全体を階層の形へ運び、pair-singleton は最後に、宣言どおりの向きで使われる。

最初の三つの因子は外側から順に書き換える。pairʟ a (pairʟ a a) における和集合の射影方程式は (unionʟ ...) .fst ≡ ⋃ ((pairʟ a (pairʟ a a)) .fst) を与える。外側の方程式 pairʟ-fst a (pairʟ a a) に関数 ⋃_ を適用すると、引数は ⋃ ⁅ (λ p → p .fst) a , (pairʟ a a) .fst ⁆ へ書き換わる。つぎに内側の方程式 pairʟ-fst a a に関数 λ w → ⋃ ⁅ (λ p → p .fst) a , w ⁆ を適用すると、⋃ ⁅ (λ p → p .fst) a , ⁅ (λ p → p .fst) a , (λ p → p .fst) a ⁆ ⁆ が得られる。内側の重複した対は pair-singleton によって一元集合と等しく、最後の因子は同じ周囲の関数の中でこの等式を用いる。

  sucʟ-fst : (a : S) → (sucʟ a) .fst ≡ sucV (a .fst)
  sucʟ-fst a =
      unionʟ-fst (pairʟ a (pairʟ a a))
    ∙ cong ⋃_ (pairʟ-fst a (pairʟ a a))
    ∙ cong (λ w → ⋃ ⁅ a .fst , w ⁆) (pairʟ-fst a a)

最後の因子は、階層自身の法則が入る場所である。pair-singleton (a .fst) は、重複した対 ⁅ (λ p → p .fst) a , (λ p → p .fst) a ⁆ を一元集合 ⁅ (λ p → p .fst) a ⁆ と同一視するパスである。同じ関数をこのパスに適用すれば、項は ⋃ ⁅ (λ p → p .fst) a , ⁅ (λ p → p .fst) a ⁆ ⁆ となり、これはまさに sucV (a .fst) である。したがってこの因子の連なりは主張を検証する。内部の後者は、基底の集合を通して読めば階層の後者なのである。

    ∙ cong (λ w → ⋃ ⁅ a .fst , w ⁆) (pair-singleton (a .fst))

数項列の構成

原始再帰により内部の零と後者から numeralL を定義し、帰納法で周囲の数項との等しさ numeralL-fst を証明する。

後者の方程式が手に入れば、列は自然数上の通常の再帰で書け、一度の帰納法で階層の数項へ射影されることが示される。第 0 の段階は内部の空集合であり、その基底の集合は文字どおり空集合である。

この節が供給するのは、各数項を台の要素として、その所属の振る舞いとともに得ることである。すべての数項を一つの集合に収集するのではなく、無限公理を証明するのでもない。列は後者の方程式の繰り返しにすぎないので、帰納法で内容のあるのは一歩だけで、零の場合は計算である。

定義は二つの節からなる。第 0 の段階は ∅ʟ、すなわち内部の空集合であり、その後の各段階は内部の後者を直前のものに適用したものである。再帰が自然数の添字の上で行われるので、列は明示的な関数 ℕ → S である。∅ʟ、pairʟ、unionʟ はいずれもそのような要素を返し、内部の後者は繰り返しのたびにこれを保つので、各段階は台の要素になっている。したがって各段階は構成可能性の証明書とともにまとめて手に入る。

  numeralL : ℕ → S
  numeralL     = ∅ʟ
  numeralL (suc n) = sucʟ (numeralL n)

  numeralL-fst : (n : ℕ) → (numeralL n) .fst ≡ # n
  numeralL-fst     = refl

周囲の数項との整列は n 上の帰納法で証明する。零では両辺とも空集合に計算されるので、パスは refl である。後続では、sucʟ-fst を numeralL n に適用して (numeralL (suc n)) .fst を sucV ((numeralL n) .fst) と同一視し、帰納法の仮定 (numeralL n) .fst ≡ # n の上の関数 sucV を帰納の一歩を後者の内部へ運ぶ。合成は # (suc n) を定義する再帰と同じ形をしているので、二つの列はすべての段階で一致する。

  numeralL-fst (suc n) = sucʟ-fst (numeralL n) ∙ cong sucV (numeralL-fst n)

二つの指定方程式

numeralL-zero は内部の零に要素がないことを示し、numeralL-suc は次の数項の要素が直前の数項の要素とその数項自身からなることを特徴づける。

モデルの record は数項列にこの二つの法則を要求する。零が空であること、そして各後者の要素が前者の要素に前者自身を加えたものにちょうど等しいこと。どちらも派生した演算ではなく所属を通して述べられている。この言い回しゆえに証明は短くなる。どちらも階層の数項についての事実であり、射影の族 numeralL-fst に沿って輸送されるからである。ここで確定記述の演算子が展開されることは一切ない。

運び役はモジュール NumPin である。これは周囲の階層に値をとる列 a : ℕ → V ℓ と整列 q : (n : ℕ) → a n ≡ # n を受け取り、その列に対する二つの指定方程式を返す。こちらの列は基底の集合の族 λ k → (numeralL k) .fst と整列 numeralL-fst を供給する。

第 0 の方程式は反駁の形をしている。列の第 0 段階の要素 z から空のホスト型の要素が得られるので、得られる関数型は hProp の設定ではそれ自身が命題である。pinZero は仮定された所属を段階 0 での整列に沿って輸送し、(numeralL zero) .fst への所属を # zero への所属に変え、その後、階層自身の「∅ には要素がない」という事実が証明を閉じる。輸送は一方向にだけ進む。列からライブラリの数項へ、である。

numeralL-zero : (z : S) → ⟨ z ∈ˢ numeralL zero ⟩ → ⊥₀
numeralL-zero z = NumPin.pinZero (λ k → (numeralL k) .fst) numeralL-fst (z .fst)

numeralL-suc : (n : ℕ) (z : S)
             → (⟨ z ∈ˢ numeralL (suc n) ⟩
                  → ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩)

後者の方程式は一対の含意であり、その第二の成分が語るのは構造の関係 ≈ˢ である。この制限構造では、その基底はパス z .fst ≡ (numeralL n) .fst である。順方向では、numeralL (suc n) の要素が段階 suc n での整列に沿って # (suc n) への所属へ輸送され、そこで階層自身の sucV の所属の分析が、単に存在するものとして、それを # n の要素である場合と # n そのものである場合に分ける。各枝はさらに段階 n での逆向きの整列に沿って列へ輸送し戻される。逆方向では、numeralL n の要素は # n へ輸送されたうえで ∈sucV-inl によって # (suc n) へ置かれ、numeralL n と等しい要素はパスを # n へ運び、階層自身の「集合は自分自身の後続に属する」という事実を使う。どちらの向きも、列 λ k → (numeralL k) .fst と整列 numeralL-fst に対する pinSuc の出力を z .fst に実例化したものである。

             × (⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
                  → ⟨ z ∈ˢ numeralL (suc n) ⟩)
numeralL-suc n z = NumPin.pinSuc (λ k → (numeralL k) .fst) numeralL-fst n (z .fst)

まとめ

numeralL は L の内部におけるフォン・ノイマン数項のコピーであり、モデルの record が要求する零と後者の正確な所属法則を満たす。

本章の議論には三つの層がある。内部の後者は、一意存在が可縮中心として手渡す演算から組み立てられ、射影方程式がそれらの演算の基底の集合を、命題の水準で、階層の非順序対・和集合・後者と同一視する。つぎに自然数上の再帰が内部の空集合から内部の後者を繰り返し、帰納法により numeralL-fst、すなわち各段階の基底の集合を周囲の数項 # n と整列させるパスの族が証明される。最後に、この整列へ NumPin を適用して numeralL-zero と numeralL-suc が従い、二つの所属法則が内部の列に対して成り立つ。場合分けの分析はすべて階層の数項の上で行われる。

ここで確立されるのは個々の数項についての事実である。各 numeralL n が L の内部に存在し、正しい所属の振る舞いをもつこと。本章には段階たちを一つの集合へ収集する主張はなく、無限は証明されない。射影方程式の用途は数項にとどまらず、モデルの対と和集合から組み立てられたものは、基底の集合を通して読めば、階層の演算から組み立てた同じものである。