---
title: "集合的小呈现"
module: V.Presentation
lang: zh
site: "Bedrock"
description: "集合的小呈现"
stage: "序数、单射与基数"
reading_order: 86
canonical: https://bedrock.institute/zh/V.Presentation.html
html: V.Presentation.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Presentation.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/V.Presentation.md, https://bedrock.institute/ja/V.Presentation.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 集合的小呈现

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

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

```agda
{-# 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 ⟫↪ _`。这份呈现是强意义下的典范：一个集合不可能带有两份这样的不同呈现。下面的引理组合的正是这些成分。

```agda
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`。这不是索引的截断存在性，而是显式构造出的索引。这一步之所以合法，是因为该嵌入的原像都是命题：截断的隶属陈述得以消去到这种原像的类型中，索引便可在其中读出。

```agda
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` 合看，这表明典范呈现对原生隶属与小隶属都是忠实的，且其索引映射既不丢失也不重复元素。

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

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