非可述性

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

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

問題は宇宙レベルに現れます。基礎型が Type ℓ に属する命題は hProp ℓ をなしますが、この命題の宇宙全体は Type (ℓ-suc ℓ) に属します。したがって、hProp ℓ のすべての命題にわたる量化から得た命題が、再びレベル ℓ に収まるとは限りません。本章では、そのような上位の命題の真理内容を、どのように下位レベルの対象で表せるかを問います。

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

module Base.Impredicativity where

open import Base.Prelude

宇宙レベルを越えた比較

上位の命題を「表す」とは、その命題をそのまま下位の宇宙へ入れることではありません。同じ内容を表す下位の命題を見つけることです。この主張を正確に書くには、まず両者をどの関係で比較するかを定める必要があります。

パスはこの役割を直接には担えません。パスの両端は共通の型に属する必要がありますが、上位と下位の命題は異なる宇宙に属するからです。論理的同値は命題間の両方向の含意を表せますが、後で用いる小分類子それ自体は命題ではありません。そこで、任意の型に使える比較として型同値を用います。

型 A と B の型同値 A ≃ B は、まず写像 f : A → B を含みます。この写像がすべての情報を保つかを調べるため、各 b : B が A からどのように写ってくるかを一つずつ考えます。

open import Cubical.Foundations.Equiv using ( _≃_ )

b 上の f のファイバーは、次の依存対型です。

ファイバーの要素は二つの成分を持ちます。第一成分は原像の候補 a : A、第二成分はその候補が実際に b へ写ることを示すパス f a ≡ b です。ファイバーが空なら b に原像はありません。ファイバーにパスで同一視できない要素があれば、b から A へ戻る方法に本質的な違いが残っています。

各 b : B 上のファイバーが可縮なら、各ファイバーには中心があり、他のすべての要素はパスによってその中心と等しくなります。したがって、すべての b を A から復元でき、その復元はパスの意味で曖昧さを残しません。この条件を満たす写像を同値と呼びます。逆写像と二つの往復パスは、各ファイバーの中心から導けます。

この型同値は同型と区別する必要があります。同型は順写像、選ばれた逆写像、二つの逆法則を明示的に与えます。同型は同値へ変換でき、同値も同型として表示できます。違いは、同じ数学的情報をどのように編成するかにあります。具体例を構成するときには、写像を明示する同型が便利なことがあります。一方、Cubical ライブラリは型の構造を運ぶ共通のインターフェースとして同値を用いるため、本章も二つの小ささの原理を _≃_ で記述します。

_≃_ は単なる論理的同値でもありません。二つの命題の論理的同値が与えるのは、両方向の含意です。P と Q の基礎型がともに isProp を満たすなら、この二つの含意から型同値を構成できます。命題性によってすべての証明が区別できなくなり、二つの合成が自動的に逆法則を満たすからです。一般の型では、両方向の写像があっても互いに逆とは限らないので、それだけでは不十分です。以下の二つの用法は、この違いを表します。isSmall では両辺が命題なので、論理的同値を型同値へ高められます。HPropSmallness では、小分類子も hProp ℓ もそれ自体は命題ではないため、完全な型同値が必要です。

以上の三つの概念は、本書の議論で異なる役割を担います。型同値を証明するときにはまず同型を構成することが多く、構造を保存して運ぶときには型同値を共通の形として用い、二つの対象が同じ型に属するところまで来れば、最後の比較をパスとして述べます。

小さいということ

P : hProp (ℓ-suc ℓ) とします。基礎型が P の基礎型と同値な Q : hProp ℓ があれば、P の真理内容はレベル ℓ に表現を持ちます。この一対のデータを持つことが、P が小さいという意味です。第一成分は Q を選び、第二成分は両側の証明を双方向に変換します。

証拠全体である isSmall P は依然として Type (ℓ-suc ℓ) に属します。小ささは P 自身を低い宇宙へ移すのではなく、低いレベルの代表を与えます。異なる証拠が異なる代表を選んでもかまいません。

isSmall : ∀ {ℓ} → hProp (ℓ-suc ℓ) → Type (ℓ-suc ℓ)
isSmall {ℓ} P = Σ[ Q ∈ hProp ℓ ] (⟨ P ⟩ ≃ ⟨ Q ⟩)

二つのインターフェース

小ささは一つの命題についての性質です。命題リサイズはこれを任意の命題に一様に与えます。レベル ℓ より一つ上の宇宙にある命題を受け取るたびに、その命題が小さいことの証拠を返します。したがって Resizing ℓ は、入力を P : hProp (ℓ-suc ℓ)、出力を isSmall P とする依存関数型です。

入力が hProp (ℓ-suc ℓ) 全体を動くため、命題リサイズ自身は Type (ℓ-suc (ℓ-suc ℓ)) に属します。その元は各 P に代表を一つ与えますが、代表の一意性も、選択された代表の間の追加の関係も要求しません。

Resizing : ∀ ℓ → Type (ℓ-suc (ℓ-suc ℓ))
Resizing ℓ = (P : hProp (ℓ-suc ℓ)) → isSmall P

第二の原理は命題の宇宙全体を扱います。HPropSmallness ℓ の証拠は、一つの型 Ω' : Type ℓ と同値 Ω' ≃ hProp ℓ を与えます。こうして、一つの小分類子がレベル ℓ のすべての命題を一度に提示します。

分類子自身が命題である必要はなく、その要素が同値を通して命題を分類します。この主張は Type (ℓ-suc ℓ) に属し、命題リサイズより一つ低い宇宙にあります。したがって二つの原理は形が異なり、どちらの定義も一方が他方を含意するとは主張しません。

HPropSmallness : ∀ ℓ → Type (ℓ-suc ℓ)
HPropSmallness ℓ = Σ[ Ω' ∈ Type ℓ ] (Ω' ≃ hProp ℓ)

二つの原理をまとめる

累積階層では二つの原理を異なる公理に用います。命題リサイズは、分出する部分集合を定める各命題に、下の宇宙にある同値な代表を与えます。小分類子は冪集合に必要な大きさの制御を与えます。そこで Impredicativity ℓ は二つの仮定を同時に記録します。二つのフィールドは Resizing ℓ と HPropSmallness ℓ をそれぞれ持ち、両者の間に整合条件はありません。

この record は、二つの成分が属するレベルのうち高い方である Type (ℓ-suc (ℓ-suc ℓ)) に属します。射影すれば、どちらの原理も独立に取り出せます。record は数学的な強さを加えず、二つの原理の連言をデータとして表すだけです。

record Impredicativity (ℓ : Level) : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    resizing       : Resizing ℓ
    hPropSmallness : HPropSmallness ℓ

まとめ

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