集合的小呈现

累积层级中集合的隶属以索引为基础，却只是弱化的形式：陈述 x ∈ a 只记录某个索引单纯存在，而且它住在比索引类型本身高一层的宇宙。因此，要在层级内部做集合论，就需要在索引与隶属证明之间往返的方法，也需要一份小而具体、且唯一的索引供给。本章记录提供这两者的基本引理。每个集合都带有典范的小呈现：一个索引类型和一张嵌入，其像正是该集合；这些引理在索引与隶属证明之间往返，记录嵌入的单射性，并把典范隶属改写成小关系的形式。后续构造依赖这套工具：讨论一个集合的元素，由此成为讨论它的索引。

这里的原始集合概念本身就是一种呈现概念。构造子 sett 从一个小索引类型和指向 V 的族，造出该族取值组成的集合；成员关系 y ∈ sett X ix 仅当某个索引 i : X 满足 ix i ≡ y 时成立；路径构造子把成员一致的两个呈现视为同一个集合。呈现由此内建于每个集合，下面的引理使它可以直接用于隶属论证。宇宙参数 ℓ 规定索引类型允许的大小，以下一切都在这个固定的层级上进行。

{-# 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