结构

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

关于集合的一阶语言有两个初始谓词：等词与隶属。要解释它，就必须选定变量的取值范围，以及这两个谓词在那里分别指什么。ZFStructure 正是打包这些数据：一个由「集合」组成的载体，加上等词与隶属的命题值解释。这个 record 只要求载体是 h-集合，别无其他；其中不内置任何 ZF 公理。

两个关系都取值于 hProp，因此每条原子陈述都有一个底层类型，其元素就是该陈述的证明。载体上的类也因而可以用来裁出较小的结构：Transitive 表达类的元素之元素仍留在类中，限制 𝒮 ↾ M 则把类变成一个由依值对组成的新结构的载体。由于各隶属纤维都是命题，这个对载体仍是 h-集合，且第一投影的相等已经决定整个对的相等。

全章要区分三种隶属记号：宿主层的类隶属 ∈ᶜ，检验载体元素是否满足谓词 M；取命题值的结构隶属 ∈ˢ；以及「对象语言」一章语法中的隶属符号 ∈̇，只有在结构给出解释之后它才有意义。

隶属出现在三个不同的层面上，记法把它们彼此分开。在宿主层，类是取值于 hProp 的谓词 M，x ∈ᶜ M 就是底层命题 ⟨ M x ⟩：一个见证 x 满足该谓词的类型。这是载体元素与谓词之间的关系，不是两个集合之间的关系。在结构层，x ∈ˢ y 是关于两个载体元素的命题。对象层属于「对象语言」一章的语法，那里的 ∈̇ 只是一个等待解释的符号。

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

module FOL.ZFStructure where

open import Base.Prelude

结构中的关系是命题，因此可以用证明占据其底层类型。把满足一个类的载体元素汇集起来，便得到依值对类型。载体 S 是 h-集合并不自动保证这样的对类型也是 h-集合；关键在于每个纤维，也就是固定元素处的隶属证据，都是命题，因此不会有两组不同的证明把本应相等的对拆开。

open import Cubical.Foundations.HLevels using ( isSetΣSndProp )

因此，把结构限制到一个类，依赖的是关于依值对的一个一般原理。对由第一投影和类型依赖于第一投影的第二分量组成。当第二分量取命题值时，就相等而言，对所携带的信息不超出第一投影：若 fst a ≡ fst b，则已经有 a ≡ b。本章以引理 ↾-reflects 收尾，为限制载体记录这个方向。

open import Cubical.Data.Sigma using ( Σ≡Prop )

结构的 record

为什么集合的等词应当是字段，而不是直接采用宿主中的路径相等？因为集合论语言把 = 与 ∈ 当作初始符号，而结构正是对它们意义的一次选定。两个载体元素即使作为宿主类型的元素并不相同，也可能被结构判为相等。把 ≈ˢ 与 ∈ˢ 做成取命题值的字段，准确写出了结构所提供的数据；这个 record 不对两种关系施加任何相容性定律。

约定全书通用：花体 𝒮 代表结构，S 代表其载体，x、y、z 代表载体元素，即这门语言所谈的「集合」。上标 ˢ 标示一个符号是当前结构的字段，纸面上的隶属记号一族已一字一层：库的 ∈ 表示宿主，∈ˢ 表示结构，对象语言中的 ∈̇ 表示语法。

这个 record 刻意只记录裸的模型论数据：要求载体是 h-集合，并给出两个命题值关系；不主张外延性、良基性或任何其他 ZF 公理。那些属于后文的模型诸章，在那里成为模型的进一步字段。

载体 S 是层级 ℓ 上的普通类型，字段 isSetS 要求它是 h-集合：其相等类型都是命题。这是对语言中「集合」可以是什么的唯一约束。两个关系字段取值于 hProp ℓ。由于 S : Type ℓ 与 hProp ℓ 都位于高一层宇宙，整个 record 的类型是 Type (ℓ-suc ℓ)。

record ZFStructure (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    S         : Type ℓ
    isSetS    : isSet S

两个关系字段给出结构的等词 ≈ˢ 与隶属 ∈ˢ，都是 S → S → hProp ℓ 型的函数。因此，x ∈ˢ y 是关于两个载体元素的命题。record 到此为止：载体与两个关系是数据，h-集合性是约束，并未施加集合论公理。

    _≈ˢ_ _∈ˢ_ : S → S → hProp ℓ

  infix 20 _≈ˢ_ _∈ˢ_

结构等词 ≈ˢ 是字段，而不是宿主的路径相等，因此任意结构都分别提供自己的真值等词解释与成员解释，record 不施加任何相容性定律。

命题侧

每个结构隶属命题都有底层类型。记号 x ∈ᵗ y 所指的恰是 ⟨ x ∈ˢ y ⟩。正是这个 Type 值读法，让后续定义能够使用隶属的证明，并把类的成员收集成依值对。模块 hPropStructure 在结构字段之上加入这个记号。

x ∈ᵗ y 定义为底层类型 ⟨ x ∈ˢ y ⟩，因此落在 Type ℓ 中。这不是新关系，而是既有隶属命题的 Type 值读法。注意实参方向与前面的记号一致：x ∈ᵗ y 读作「x 是 y 的成员」。

module hPropStructure {ℓ} (𝒮 : ZFStructure ℓ) where
  open ZFStructure 𝒮 public

  _∈ᵗ_ : S → S → Type ℓ
  x ∈ᵗ y = ⟨ x ∈ˢ y ⟩

于是 y ∈ᵗ x 陈述的是：在命题值结构中 y 是 x 的成员；这个类型的元素，就是成员真值成立的证据。

  infix 20 _∈ᵗ_

传递类

隶属以 Type 值命题的形式可用之后，载体上的类就成为可以逐个元素推理的对象。类 M 若使 M 中元素的每个成员仍属于 M，就称为传递。这是集合论中的传递性概念，用现有的两种隶属关系来表述：蕴涵左侧用结构的 ∈ᵗ，类本身的隶属用宿主层的 ∈ᶜ。

Transitive 接受命题值结构 𝒮 与类 M : S → hProp ℓ，陈述蕴涵 y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M：若在结构中 y 是 x 的成员，且 x 属于类 M，则 y 也属于 M。这里的方向是对元素之元素的闭合，而不是对子集的闭合；定义隐含地量化载体元素 x、y，此外不断言任何内容。

Transitive : ∀ {ℓ} (𝒮 : ZFStructure ℓ)
           → (ZFStructure.S 𝒮 → hProp ℓ) → Type ℓ
Transitive 𝒮 M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M
  where open hPropStructure 𝒮

子结构

给定命题值类 M，现在可以把结构裁剪到载体中满足 M 的那一部分。限制 𝒮 ↾ M 仍是一个 ZFStructure，其载体是依值对 (x , proof) 的类型，其中 x : S 且 proof : x ∈ᶜ M。限制元素上的等词与隶属从 𝒮 继承：两种关系都只看第一投影，并在其上应用原关系。这改变的是结构中什么算作元素；它不构造表示 M 的集合，也不自行确定语法或常元域。

新载体是 Σ 类型 Σ[ x ∈ S ] (x ∈ᶜ M)：其元素是「底层载体元素配上 M 的成员证据」的对，因此限制并不把 M 收集成一个集合，只是改变哪些对算作元素。record 的 isSetS 字段仍须填写，这里正是章首那条逐纤维的事实起作用：由于每个 M x 凭第二分量是命题，把 isSetΣSndProp 作用于 isSetS 便证明这个对类型仍是 h-集合。

_↾_ : ∀ {ℓ} (𝒮 : ZFStructure ℓ)
    → (ZFStructure.S 𝒮 → hProp ℓ) → ZFStructure ℓ
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∈ S ] (x ∈ᶜ M)
  ; isSetS = isSetΣSndProp isSetS (λ x → (M x) .snd)

两个关系字段都沿第一投影拉回原关系：对限制元素 a、b，结构求值 fst a ≈ˢ fst b 与 fst a ∈ˢ fst b。因此限制元素之间的隶属与相等完全在其底层载体元素上求值；对在第二分量携带的证据对这两种关系不起任何作用。

  ; _≈ˢ_   = λ a b → fst a ≈ˢ fst b
  ; _∈ˢ_   = λ a b → fst a ∈ˢ fst b }
  where open ZFStructure 𝒮

infixl 21 _↾_

𝒮 ↾ M 的关系忽略第二分量，于是可以问：限制载体除了第一投影之外，是否还能区分不同的对？不能：因为每个隶属类型 M x 都是命题，第一投影之间的路径决定整个对之间的路径。下面的引理记录这个方向。

↾-reflects 的类型是 fst a ≡ fst b → a ≡ b。它把 Σ≡Prop 用于族 λ x → (M x) .snd，该族逐点证明 x 处的成员证据是命题；于是对之间的路径仅由第一投影之间的路径构成。该引理只陈述这一个方向：底层元素的相等被反映为限制元素的相等，不另行陈述逆向命题。

↾-reflects : ∀ {ℓ} {𝒮 : ZFStructure ℓ} {M : ZFStructure.S 𝒮 → hProp ℓ}
             {a b : ZFStructure.S (𝒮 ↾ M)}
           → fst a ≡ fst b → a ≡ b
↾-reflects {M = M} = Σ≡Prop (λ x → (M x) .snd)

小结

ZFStructure 记录四个字段：载体、载体的 h-集合性证明，以及等词与成员关系的真值解释；其中不包含 ZF 公理。对命题值结构，∈ᵗ 给出成员真值的底层类型，Transitive 陈述对元素之元素的闭合，𝒮 ↾ M 把载体限制到一个由依值对组成的类。引理 ↾-reflects 把第一投影的相等提升为限制载体中的相等。下一步是在这样的结构中解释对象语言的公式本身。