集合の小さな提示

累積階層の集合への所属はインデックスを基礎としますが、弱められた形にすぎません。主張 x ∈ a はあるインデックスが単に存在することを記録するだけで、しかもインデックス型そのものより一つ上の宇宙に住みます。したがって階層の中で集合論を行うには、インデックスと所属証明の間を行き来する方法と、小さく、具体的で、一意なインデックスの供給が必要になります。本章はその両方を与える初等的な補題を記録します。すべての集合は正準的な小さな提示、すなわちその像がその集合であるインデックス型と埋め込みを伴い、補題はインデックスと所属証明の間を行き来し、埋め込みの単射性を記録し、正準的な所属を小関係の形で言い直します。後の構成はこの一式に依拠します。集合の要素について論じることは、そのインデックスについて論じることになるのです。

ここでの原始的な集合概念は、それ自体がすでに提示の概念です。構成子 sett は、小さなインデックス型と V への族から、その族の値のなす集合を形作ります。所属 y ∈ sett X ix は、ix i ≡ y となるインデックス i : X が切り詰められた形で存在するときに成り立ちます。そしてパス構成子は、要素の一致する二つの表示を同一視します。提示はこのようにすべての集合に組み込まれており、以下の補題はそれを所属の議論で直接使えるようにします。宇宙パラメータ ℓ がインデックス型に許される大きさを定め、以下はすべてこの固定されたレベルに相対的です。

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

open import Base.Prelude

module V.Presentation {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

同じ所属の事実には二つの形があり、以下の補題はその間を行き来します。構造 𝒮ᵥ では、所属は命題 x ∈ˢ y として読まれます。その証明は切り詰められた存在言明であり、インデックスを伴いません。これに対して小所属 a ∈ₛ b は同値な命題であり、ℓ-suc ℓ ではなくレベル ℓ に住みます。その基礎型は、b のインデックスと、名指された要素が a と双シミュレーションの意味で一致することの証明の組を要求します。各集合 a には選ばれた提示があります。小さなインデックス型 ⟪ a ⟫、階層への埋め込み ⟪ a ⟫↪ (その埋め込みの性質は isEmb⟪ a ⟫↪ が記録します)、そしてそのインデックスそれぞれへの小所属の証明 ∈ₛ⟪ a ⟫↪ _ です。この提示は強い意味で正準的です。ひとつの集合が、この種の異なる提示を二つ持つことはありません。以下の補題はまさにこれらの材料を組み合わせます。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber )

open hPropStructure 𝒮ᵥ

最初の二つの補題は、インデックスと所属証明を相互に変換します。鍵となるのは ∈∈ₛ で、本来の所属と小所属が一致することを、二つの含意の組として述べます。補題 member はインデックス m : ⟪ a ⟫ を取り、小から本来への含意を証明 ∈ₛ⟪ a ⟫↪ m に適用し、⟪ a ⟫↪ m ∈ˢ a の要素を生み出します。これは、インデックス m の指す要素が集合 a に属することの明示的な証明です。逆の fiber は x ∈ˢ a の証明から出発し、実際のインデックス m : ⟪ a ⟫ とパス ⟪ a ⟫↪ m ≡ x の組を返します。これはインデックスの切り詰められた存在ではなく、明示的に構成されたインデックスです。この一段階が正当なのは、埋め込みのファイバーが命題値だからです。切り詰められた所属の主張はこのファイバーの型へ消去でき、そこでインデックスを読み取れます。

member : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ˢ a ⟩
member a m = ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)

fiber : (a : S) {x : S} → ⟨ x ∈ˢ a ⟩ → Σ[ m ∈ ⟪ a ⟫ ] (⟪ a ⟫↪ m ≡ x)
fiber a {x} x∈ = ∈-asFiber {a = x} {b = a} x∈

↪-inj : {a : S} {m n : ⟪ a ⟫} → ⟪ a ⟫↪ m ≡ ⟪ a ⟫↪ n → m ≡ n

短い二つの事実が全体を完成させます。埋め込みの性質とは、インデックス上の単射性のことです。h-集合への埋め込みは命題値のファイバーを持ち、標準補題 isEmbedding→Inj はそこから「値が等しければインデックスも等しい」を導きます。これを ↪-inj が記録します。最後に ∈ₛ↪ は小所属を直接述べます。各インデックス m に対し、要素 ⟪ a ⟫↪ m は証明 ∈ₛ⟪ a ⟫↪ m とともに小所属の意味で a に属します。member と併せて、正準的な提示が本来の所属と小所属のどちらに対しても忠実であり、そのインデックス写像が要素を失わず複製しないことが示されます。

↪-inj {a} {m} {n} = isEmbedding→Inj isEmb⟪ a ⟫↪ m n

∈ₛ↪ : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ₛ a ⟩
∈ₛ↪ a m = ∈ₛ⟪ a ⟫↪ m