结构

上一章规定了关于集合的陈述可以怎样写，却还没有说明它们何时成立。要讨论一条陈述是否成立，首先要选定它所谈论的对象，再为「两个对象相等」和「一个对象属于另一个」给出解释。这些数据合在一起，就构成一个结构。

本章先定义结构，再把对象的范围限制为满足某种性质的那些对象，构造相应的限制结构。整个过程不假设任何集合论公理。

载体与关系

在对象语言中，t ≐ u 与 t ∈̇ u 是公式，还不是可以证明的命题。要解释它们，先选定一个类型 S，用它的元素表示所讨论的对象，再在 S 上给出相等与成员关系。类型 S 称为结构的载体。我们把整个结构记作 𝒮，把载体中的元素记作 x、y；关系记号上的 ˢ 则表示该关系由 𝒮 提供。

为什么相等关系也要单独给出，而不直接采用 Agda 的路径相等 x ≡ y？因为对象语言中的相等记号可以有自己的解释，不必预先等同于路径相等。结构中的 x ≈ˢ y 给出一个真值，并不要求先有一条路径 x ≡ y。在这个定义中，≈ˢ 只是一个二元关系：我们既不要求它满足相等关系的定律，也不要求它与成员关系相容。

定义 (ZFStructure) 给定载体的层级 ℓ 和真值类型 Ω，用 record 定义结构。其字段包括载体 S : Type ℓ、S 为 h-集合的证明，以及两个类型为 S → S → Ω 的关系，分别解释相等与成员关系。Ω 的层级不必与 ℓ 相同。这样，底层定义保持一般性，真值类型可以独立选择。两种关系都不附加任何定律。

record ZFStructure (ℓ : Level) {ℓΩ : Level} (Ω : Type ℓΩ)
  : Type (ℓ-max (ℓ-suc ℓ) ℓΩ) where
  field
    S         : Type ℓ
    isSetS    : isSet S

余下两个字段各自接收两个载体元素，并返回一个真值。因此，x ∈ˢ y 是 Ω 中的一个值，而上一章的 t ∈̇ u 只是一段语法。这个 record 只提供载体和关系，不规定词项怎样指代载体元素，也不要求两种关系满足集合论公理。

    _≈ˢ_ _∈ˢ_ : S → S → Ω

  infix  _≈ˢ_ _∈ˢ_

定义 (ZFStructureₕ) 取 hProp ℓ 为真值类型 Ω，得到下文使用的命题值结构。下标 ₕ 表示这一选择，其中命题与载体处于同一层级 ℓ。这只是原定义的一个特例，不另设 record。

ZFStructureₕ : (ℓ : Level) → Type (ℓ-suc ℓ)
ZFStructureₕ ℓ = ZFStructure ℓ (hProp ℓ)

ZFStructure 这个名字表明它解释的是集合论语言，并不表示它已经是 ZF 模型。例如，可以用自然数作载体，用通常的大小关系解释成员关系。即使提供了定义所要求的全部数据，也不能仅凭这些数据断言 ZF 公理成立。

命题值结构

在命题值结构 ZFStructureₕ 中，x ∈ˢ y 包含一个类型，以及该类型为命题的证明。若要把「x 属于 y」的证明作为函数实参，就需要取出底层类型 ⟨ x ∈ˢ y ⟩。子模块 hPropView 固定结构 𝒮，将这个类型简记为 x ∈ᵗ y。

module hPropView {ℓ} (𝒮 : ZFStructureₕ ℓ) where

open ZFStructure 𝒮 public

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

Transitive : (S → hProp ℓ) → Type ℓ
Transitive M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M

这几个成员关系记号写法相近，含义却不同。还要注意，类由谓词 M : S → hProp ℓ 给出。因此，x ∈ᶜ M 表示元素 x 满足谓词 M，说的不是两个载体元素之间的关系。

子结构

若要让变元只在 M 选中的元素中取值，就需要更换载体。仅仅给出谓词 M，却仍以整个 S 为载体，并不能限制取值范围。因此，新载体的每个元素都由两部分组成：一个 x : S，以及 x ∈ᶜ M 的证明。把结构 𝒮 限制到类 M 所得的结构，记作 𝒮 ↾ M。

限制结构不要求类具有传递性，也不要求原结构的关系取命题值：真值类型 Ω 可以任意选择，只有筛选载体元素的谓词需要取命题值。下面在本模块中打开载体相关的字段投影，两个关系则留到使用时再针对具体结构打开。与 hPropView 内的打开方式不同，这里不固定结构，而是在使用各投影时传入结构，例如用 S 𝒮 取得 𝒮 的载体。其中，𝒮 的作用相当于数学记号中 S 的下标，指明这是哪个结构的载体；在 Agda 中，它仍是普通的函数实参。

open ZFStructure using ( S; isSetS )

定义 (_↾_) 给定类 M : S → hProp ℓ，限制结构的载体为 Σ[ x ∶ S ] (x ∈ᶜ M)。这是一个依值对类型，并不是在原结构内部找到了一个代表类 M 的集合。原载体是 h-集合，而每个元素属于 M 的证明类型都是命题，因此可用前文引入的 isSetClass 证明新载体也是 h-集合。

infixl  _↾_
_↾_ : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} (𝒮 : ZFStructure ℓ Ω)
    → (S 𝒮 → hProp ℓ) → ZFStructure ℓ Ω
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∶ S 𝒮 ] (x ∈ᶜ M)
  ; isSetS = isSetClass (isSetS 𝒮) (λ x → ⟨ M x ⟩isProp)

新载体上的两种关系怎样定义？给定其中的元素 a、b，先取出各自的第一分量，再应用 𝒮 的关系，得到 a .fst ≈ˢ b .fst 与 a .fst ∈ˢ b .fst。下面的定义只在局部打开原结构的这两个关系。第二分量只证明第一分量属于 M，不影响这两种关系的真值。也就是说，新关系是原关系沿第一投影 fst 的拉回。

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

这两种关系都只用到第一分量。那么，两个依值对本身是否相等，会不会受到第二分量的影响？这里讨论的是 Agda 的路径相等，而不是结构中另行指定的关系 ≈ˢ。

引理 (↾-reflects) 给定限制结构的载体元素 a、b，由路径 a .fst ≡ b .fst 可得路径 a ≡ b。

证明 沿第一分量之间的给定路径，传输其中一份证明。传输后，两份证明属于同一个命题，因而相等，由此得到两个依值对之间的路径。库引理 Σ≡Prop 完成这一构造；所需的条件由 ⟨ M x ⟩isProp 给出，即每个第二分量的类型都是命题。

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

反方向更直接：将 fst 作用于路径 a ≡ b，就得到 a .fst ≡ b .fst，无需另设引理。

小结

结构给出了所讨论的对象，以及相等和成员关系的解释。无论结构选用什么真值，都可以用命题值谓词限制载体，并继承原来的两种关系；附带的成员关系证明不会区分第一分量相等的依值对。对于命题值结构，传递性是另一项独立条件，要求被选中对象的元素也留在选定范围内。下一章将在选定的结构中解释词项与公式。