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

対話型目次 · 依存グラフ

直謂的な基礎では、一つの定義の中で、定義される対象をすでに含む全体にわたって量化することを認めない。Cubical Agda はこのような基礎の上にあるが、本書で形式化する集合論には非可述的な構成が含まれる。そこで本章では、ホストの基礎そのものを変えずに、それらの構成に必要な追加条件を明示的な仮定として述べる。

直謂的な基礎が非可述的な仮定を受け入れられることは、直観主義論理が古典論理の原理を明示的に仮定できることに似ている。逆は成り立たない。強い原理を初めから基礎に組み込めば、後の結果がそのどれに依存するかを区別できなくなるからである。本書は Cubical Agda の直謂的な基礎を保ち、非可述性が必要な箇所で条件を一つずつ明記する。

問題は宇宙レベルに現れる。基礎型が Type ℓ に属するすべての命題は hProp ℓ をなすが、この命題の宇宙全体は Type (ℓ-suc ℓ) に属する。したがって、hProp ℓ のすべての命題にわたる量化から得た命題が、再びレベル ℓ に収まるとは限らない。

例えば、命題 R を「すべての Q : hProp ℓ は自分自身を含意する」と定義し、同時に R も hProp ℓ に属すると要求してみる。このとき、定義中の「すべての Q」は R 自身にも及ぶ。量化する全体が、定義中の命題をすでに含んでいるのである。「Q は自分自身を含意する」という主張は明らかであるが、その量化から得た命題を同じレベルに置くという要求が問題である。Cubical Agda では、この量化は一つ上の宇宙に属する。Agda のユーザーコードから宇宙レベルの規則を書き換えることはできないが、明示的な仮定によって、上位の命題と真理内容が同じ下位の代表を結び付けられる。

この結び付きには、基礎語彙で導入した型同値 A ≃ B を使う。これは、異なる宇宙の型を、その要素とパスを保ちながら結び付けられる。以下では、各命題の代表を個別に求めることと、命題の宇宙全体を一つの型で提示することという、二つの大きさの要求を区別する。

命題リサイズ

P : hProp ℓ₁ が与えられても、Agda では P の属するレベルを直接変更できない。代わりに、目標レベルの別の命題 Q : hProp ℓ₂ を見つけ、その基礎型が P の基礎型と型同値であることを要求できる。

定義 (hasSize) ここでは「P はサイズ ℓ₂ をもつ」を hasSize ℓ₂ P と表し、次の依存対として定義する。第一成分は Q を選び、第二成分は Q と P の真理内容が完全に一致することを示す型同値を与える。

hasSize : ∀ {ℓ₁} (ℓ₂ : Level) → hProp ℓ₁ → Type (ℓ-max ℓ₁ (ℓ-suc ℓ₂))
hasSize ℓ₂ P = Σ[ Q ∶ hProp ℓ₂ ] (⟨ P ⟩ ≃ ⟨ Q ⟩)

二つのレベルの大小関係は仮定しない。後の応用では通常、ℓ₁ はモデルの真理値のレベル、ℓ₂ は添字のレベルであるが、定義そのものは任意の二つのレベルに適用できる。「命題リサイズ」とは、元の命題の宇宙注釈を変更することではなく、目標レベルにある型同値な代表で置き換えることを指す。

定義 (Resizing) ここでは「レベル ℓ₁ の命題をレベル ℓ₂ へリサイズできる」を Resizing ℓ₁ ℓ₂ と表し、次の依存関数として定義する。各 P : hProp ℓ₁ に対して、「P はサイズ ℓ₂ をもつ」ことの証拠を返す。

Resizing : ∀ ℓ₁ ℓ₂ → Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂))
Resizing ℓ₁ ℓ₂ = (P : hProp ℓ₁) → hasSize ℓ₂ P

命題宇宙リサイズ

定義 (ΩResizing) ここでは「命題宇宙 hProp ℓ₁ はサイズ ℓ₂ をもつ」を ΩResizing ℓ₁ ℓ₂ と表し、次の依存対として定義する。第一成分は型 Ω : Type ℓ₂ を与え、第二成分は型同値 hProp ℓ₁ ≃ Ω を与える。したがって、レベル ℓ₁ の各命題は Ω に符号をもち、Ω の各要素はそのレベルの命題へ復号される。

ΩResizing : ∀ ℓ₁ ℓ₂ → Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂))
ΩResizing ℓ₁ ℓ₂ = Σ[ Ω ∶ Type ℓ₂ ] (hProp ℓ₁ ≃ Ω)

命題リサイズ

命題リサイズは、各命題を指定した宇宙レベルにある型同値な代表で置き換える。

$$r : \operatorname{Resizing}\,\ell_1\,\ell_2$$
$$P_i : \operatorname{hProp}\,\ell_1$$
$$Q_i : \operatorname{hProp}\,\ell_2$$
$$\langle P_1\rangle$$
$$\overset{e_1}{\simeq}$$
$$\langle Q_1\rangle$$
$$\langle P_2\rangle$$
$$\overset{e_2}{\simeq}$$
$$\langle Q_2\rangle$$
$$\vdots$$
$$\vdots$$
$$r(P_i) = (Q_i,e_i)$$

命題宇宙リサイズ

命題宇宙リサイズは、命題宇宙全体を指定した宇宙レベルの型で提示する。

$$(\Omega,e) : \Omega\operatorname{Resizing}\,\ell_1\,\ell_2$$
$$\operatorname{hProp}\,\ell_1$$
$$P_1$$
$$P_2$$
$$\cdots$$
$$\overset{e}{\simeq}$$
$$\Omega : \operatorname{Type}_{\ell_2}$$
$$c_1$$
$$c_2$$
$$\cdots$$
$$c_i = \operatorname{equivFun}\,e\,P_i : \Omega$$

個々の命題のリサイズと命題宇宙全体のリサイズは、異なるデータを要求する

次に、命題宇宙リサイズから命題リサイズが従うことを証明する。Ω : Type ℓ₂ と同値 e : hProp ℓ₁ ≃ Ω が与えられたとする。この同値によって各命題は Ω に符号をもつが、その符号からレベル ℓ₂ の命題を構成し、元の命題との同値を示す必要がある。

通常の数学の証明なら、「以下、Ω と e を固定する」と述べ、この共通の仮定のもとでいくつかの構成を行う。Agda では、引数を持つ部分モジュール CodedTruth が同じ役割を果たす。モジュール宣言に共通のデータを並べておけば、内部の定義は毎回引数を書き直さずにそれらを使える。最後に主定理へ具体的な (Ω , e) が与えられたとき、これらの構成を呼び出す。private はこのモジュールを本章内の補助的な道具に限るだけで、新しい数学的仮定を加えない。

private module CodedTruth {ℓ₁ ℓ₂} (Ω : Type ℓ₂) (e : hProp ℓ₁ ≃ Ω) where

e の順写像を c と名付ける。すると c P が Ω における P の符号になる。

c : hProp ℓ₁ → Ω
c = equivFun e

構成 (codedTruth) 符号 c P は Ω の一点である。命題を得るには、それが真の命題の符号と等しいかを問えばよい：c ⊤ ≡ c P。このパス型はレベル ℓ₂ に属する。e が hProp ℓ₁ の h-集合構造を Ω へ運ぶので、これは命題である。これを P の代表とし、以下の同型によって真理内容が等しいことを確かめる。

codedTruth : hProp ℓ₁ → hProp ℓ₂
codedTruth P = (c ⊤ ≡ c P) , isOfHLevelRespectEquiv 2 e isSetHProp _ _

Ω の帯状領域は、端点を c(⊤)、c(P) とするパスの族を表す。クリックすると、この族が第二の型の空間へ広がり、パス全体がその点として描かれる。図の q、r は P の証明を前提とするが、⟨ P ⟩ との型同値そのものにはこの仮定は不要である。

$$\langle P\rangle$$
$$: \operatorname{Type}_{\ell_1}$$
$p$
$\simeq$
$$\langle\operatorname{codedTruth}\,P\rangle$$
$$: \operatorname{Type}_{\ell_2}$$
$q$ $r$
$$\Omega$$
$$: \operatorname{Type}_{\ell_2}$$
$q$ $\langle\operatorname{codedTruth}\,P\rangle$ $r$ $c(\top)$ $c(P)$

⟨ codedTruth P ⟩ の一点は、Ω の一本のパスそのものである：⟨ codedTruth P ⟩ = (c(⊤) ≡ c(P))。二つの証明の型はそれぞれレベル ℓ₁ と ℓ₂ に属し、互いに型同値である

補題 (codedTruthIso) P の基礎型は codedTruth P の基礎型と同型である。したがって、上で構成した代表は確かに P と同じ真理内容をもつ。

codedTruthIso : (P : hProp ℓ₁) → Iso ⟨ P ⟩ ⟨ codedTruth P ⟩

証明 二方向の写像 to と from を構成し、iso でまとめる。始域 ⟨ P ⟩ と終域 ⟨ codedTruth P ⟩ はどちらも命題なので、二つの写像を与えれば、両端の命題性が二つの往復則を直接証明する。写像が真の命題の要素を返す箇所では、その唯一の要素 tt* を明示する。

codedTruthIso P = iso to from (λ q → ⟨ codedTruth P ⟩isProp _ q) (λ p → ⟨ P ⟩isProp _ p)
  where

あとは二方向の写像を構成する。

  to : ⟨ P ⟩ → ⟨ codedTruth P ⟩
  to p = cong c (⇔toPath (λ _ → p) (λ _ → tt*))

  from : ⟨ codedTruth P ⟩ → ⟨ P ⟩
  from q = subst ⟨_⟩ (invEq (congEquiv e) q) tt*

定理 (ΩResizing→Resizing) 命題宇宙リサイズは命題リサイズを導く。

証明 (Ω , e) が与えられると、先のモジュールは各 P に対してレベル ℓ₂ の codedTruth P を与える。codedTruthIso P を isoToEquiv で同値に変換すれば、その対が hasSize ℓ₂ P となる。

ΩResizing→Resizing : ∀ {ℓ₁ ℓ₂} → ΩResizing ℓ₁ ℓ₂ → Resizing ℓ₁ ℓ₂
ΩResizing→Resizing (Ω , e) P = codedTruth P , isoToEquiv (codedTruthIso P)
  where open CodedTruth Ω e

まとめ

これらの定義は、直謂的な宇宙レベルからは自動的に得られない大きさの情報を切り分ける。同値によって上位の命題は同じ真理内容をもつ低いレベルの代表を得る。命題リサイズはその代表を各命題に与え、命題宇宙リサイズは命題の宇宙全体を一度に提示する。本章では、これらの原理の証拠をまだ構成していない。「古典論理との境界」の章で排中律から両者を導く。