構造

前章では集合についてどのような主張を書けるかを定めたが、その主張がいつ成り立つかはまだ決めていない。書かれた主張の意味を定めるには、そこで指す対象の範囲と、二つの基本的な関係、すなわち対象どうしの等しさと所属をどう判定するかを選ぶ必要がある。その選択を与えるのが構造である。

本章ではまず構造に必要なデータを定め、続いて、ある性質を満たす対象だけに制限した構造を作る。ここでは集合論の公理を仮定しない。

台と関係

対象言語の t ≐ u と t ∈̇ u は論理式であり、まだ証明できる命題ではない。その意味を定めるには、対象の型 S と、その上の二つの関係を選ぶ。得られる構造を 𝒮、その台 S の元を x、y と書く。上付きの ˢ は、関係が構造 𝒮 から与えられることを示す。

等号の関係まで別に与え、Agda のパス等式 x ≡ y をそのまま使わないのはなぜか。対象言語の等号には独自の解釈が必要だからである。パス x ≡ y が与えられていなくても、フィールド x ≈ˢ y は真理値を与えられる。この段階では単なる二項関係であり、等号の法則も、所属との整合性もまだ要求しない。

定義 (ZFStructure) 台がレベル ℓ にあるとき、このレコードは真理値の型 Ω を引数に取る。フィールドは台 S : Type ℓ、S が h-集合である証明、および等号と所属を解釈する二つの S → S → Ω 型の関係である。Ω のレベルは ℓ と一致しなくてもよい。基礎となる定義をこのように一般的に保ち、具体的な真理値は別に選ぶ。この時点で二つの関係には法則を課さない。

record ZFStructure (ℓ : Level) {ℓΩ : Level} (Ω : Type ℓΩ)
  : Type (ℓ-max (ℓ-suc ℓ) ℓΩ) where
  field
    S         : Type ℓ
    isSetS    : isSet S

残る二つのフィールドは、台の元の組ごとに真理値を与える。x ∈ˢ y の値は Ω に属するが、前章の t ∈̇ u はまだ構文にすぎない。このレコードは、項が台の元をどう指すかも、二つの関係が集合論の公理を満たすかどうかも定めない。

    _≈ˢ_ _∈ˢ_ : S → S → Ω

  infix  _≈ˢ_ _∈ˢ_

定義 (ZFStructureₕ) 以下で使う命題値の構造では、真理値の型 Ω に hProp ℓ を選ぶ。添字 ₕ は台のレベルでこの選択を表し、別のレコードを導入しない。

ZFStructureₕ : (ℓ : Level) → Type (ℓ-suc ℓ)
ZFStructureₕ ℓ = ZFStructure ℓ (hProp ℓ)

ZFStructure という名前は解釈する記号が集合論の言語に属することを示すのであって、すでに ZF のモデルであるという意味ではない。たとえば自然数を台とし、通常の大小関係を所属のフィールドに入れても、ここで必要なデータはそろう。しかしそれだけで ZF の公理が証明されるわけではない。

命題値の構造

ZFStructureₕ では、フィールド x ∈ˢ y は hProp、すなわち命題とその証明無関係性を返す。その命題の証明を関数の引数として使うには、基礎となる型 ⟨ x ∈ˢ y ⟩ を取り出す。部分モジュール hPropView は構造 𝒮 を固定し、この型を x ∈ᵗ y と書けるようにする。

module hPropView {ℓ} (𝒮 : ZFStructureₕ ℓ) where

open ZFStructure 𝒮 public

infix  _∈ᵗ_
_∈ᵗ_ : S → S → Type ℓ
x ∈ᵗ y = ⟨ x ∈ˢ y ⟩

Transitive : (S → hProp ℓ) → Type ℓ
Transitive M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M

よく似た所属の記法にも、それぞれ異なる役割がある。特にクラスは述語 M : S → hProp ℓ である。したがって x ∈ᶜ M は元がその述語を満たすかを問い、台の二つの元を比較するものではない。

部分構造

変数が M に選ばれた元だけを動くようにするには、台を作り直す必要がある。元の型 S を残して横に M を添えるだけでは、S 型の変数は選ばれなかった元も指せてしまう。そこで新しい台の各元を、x : S と x ∈ᶜ M の証拠の組にする。𝒮 ↾ M は、構造 𝒮 をこのクラスへ制限したものを表す。

構造の制限には、クラスの推移性も、関係が命題に値を取るという条件も要らない。真理値の型 Ω は任意であり、台の元を選ぶ述語だけが命題値であればよい。以下では台に関するフィールドの射影をモジュールのスコープで開き、二つの関係は使う場所で構造を固定して開く。hPropView の内部とは異なり、構造は固定せず、S 𝒮 のように各射影へ構造を引数として渡す。ここで 𝒮 は、数学の記法で S に付ける添字に相当し、どの構造の台かを指定する。ただし Agda では通常の関数の引数である。

open ZFStructure using ( S; isSetS )

定義 (_↾_) 任意のクラス M : S → hProp ℓ に対し、制限された構造の台を Σ[ x ∶ S ] (x ∈ᶜ M) とする。これは依存対の型であり、構造の内部でそのクラスを表す集合ではない。先に導入した isSetClass を isSetS と各点で所属の型が命題であることに適用し、新しい台の h-集合性を得る。

infixl  _↾_
_↾_ : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} (𝒮 : ZFStructure ℓ Ω)
    → (S 𝒮 → hProp ℓ) → ZFStructure ℓ Ω
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∶ S 𝒮 ] (x ∈ᶜ M)
  ; isSetS = isSetClass (isSetS 𝒮) (λ x → ⟨ M x ⟩isProp)

新しい台の上で二つの関係をどう定めるか。制限された元 a、b の第一射影に 𝒮 の関係を適用し、a .fst ≈ˢ b .fst と a .fst ∈ˢ b .fst を得る。以下の定義では、元の構造のこの二つの関係だけを局所的に開く。第二成分の証拠は元が M に属することを保証するだけで、等号や所属の真理値を変えない。つまり二つの関係を fst に沿って 𝒮 から引き戻す。

  ; _≈ˢ_   = λ a b → a .fst ≈ˢ b .fst
  ; _∈ˢ_   = λ a b → a .fst ∈ˢ b .fst }
  where open ZFStructure 𝒮 using ( _≈ˢ_; _∈ˢ_ )

二つの関係は第一成分だけを使う。それでは、依存対そのものの等しさは第二成分の証拠に左右されるだろうか。ここで扱うのは Agda のパス等式であり、自由に与えた構造の関係 ≈ˢ ではない。

補題 (↾-reflects) 制限された台の a、b について、パス a .fst ≡ b .fst からパス a ≡ b が定まる。

証明 第一成分の間に与えられたパスに沿って、一方の証拠を移す。移した後の二つの証拠は同じ命題に属するので等しく、依存対の間のパスが得られる。この構成はライブラリの補題 Σ≡Prop が行う。その前提である各ファイバーの命題性は ⟨ M x ⟩isProp が与える。

↾-reflects : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} {𝒮 : ZFStructure ℓ Ω}
             {M : S 𝒮 → hProp ℓ} {a b : S (𝒮 ↾ M)}
           → a .fst ≡ b .fst → a ≡ b
↾-reflects {M = M} = Σ≡Prop (λ x → ⟨ M x ⟩isProp)

逆向きに特別な補題は要らない。パス a ≡ b に fst を作用させれば a .fst ≡ b .fst が得られる。

まとめ

構造は、考察する対象の台と、等号・所属の解釈を与える。真理値の型によらず、二つの関係を受け継ぎながら、命題値の述語で台を制限できる。添えられた所属の証拠は、第一成分が等しい依存対を区別しない。命題値の構造では、推移性はこれとは独立の条件であり、選ばれた対象に属する要素も選ばれた範囲に残ることを要求する。次章では、選んだ構造の中で項と論理式に意味を与える。