集合の小さな提示

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

module V.Presentation {ℓ : Level} where

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

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

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

open hPropView 𝒮ᵥ

最初の二つの補題は、インデックスと所属証明を相互に変換する。鍵となるのは ∈∈ₛ で、本来の所属と小所属が一致することを、二つの含意の組として述べる。補題 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