Structures

公式自身没有含义；它需要一个被谈论的世界。对上一章的语言而言，世界就是模型论意义上的结构：一个载体，连同两个谓词符号 (成员与等词) 的解释，取值于选定的真值代数。本章定义这些结构、裁剪它们的方式，以及将把结构元素喂给公式的环境。

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

module FOL.ZFStructure where

open import Base.Prelude
open import Base.Truth
open import Cubical.Foundations.HLevels using ( isSetΣSndProp )
open import Cubical.Data.Sigma using ( Σ≡Prop )

结构的 record

仍先立约定，全书通用：花体 𝒮 代表结构，S 代表其载体，x、y、z 代表载体元素，即这门语言所谈的「集合」。两个关系字段上的上标 ˢ 是又一枚层标记：它宣告一个符号是当前结构的字段。至此 ∈ 家族在纸面上已有三员，一字一层：库的 ∈ (宿主)、本章的 ∈ˢ (结构)、上一章的 ∈̇ (语法)。

record ZFStructure {ℓ ℓ'} (𝕋 : TruthAlgebra ℓ ℓ') : Type (ℓ-max (ℓ-suc ℓ) ℓ') where
  open TruthAlgebra 𝕋
  field
    S         : Type ℓ
    isSetS    : isSet S
    _≈ˢ_ _∈ˢ_ : S → S → Ω

  infix 20 _≈ˢ_ _∈ˢ_

关于字段的两点。结构等词 ≈ˢ 是字段而非硬连到宿主的路径相等，这一点是承重的：在本书的力迫部分，等词与成员将是一对互递归定义的分级关系，是模型的真实内容，任何元层相等都供应不了。命题侧则毫无损失，届时装配本书实例的层级章径直以路径充当 ≈ˢ。

再说说这里没有的东西：公理。这个 record 是裸结构；良基、外延等等属于第二部，在那里它们将成为模型的字段。本部构建的一切只消费上面三个投影，于是任何两个同构的结构，按宿主的结构等同原理，干脆就相等，整个开发沿之搬运。

命题侧

命题侧还有一种成员形式可用：把 x ∈ˢ y 的底层类型取出来。上标 ᵗ 标记这个 Type 值的变体；良基性的陈述与按成员归纳的证明都将对它量化。它住在 hPropStructure 里，即命题侧打开结构的方式：该模块公开再导出三个投影并添上 ∈ᵗ，一次 open 之后，章节径直写 y ∈ᵗ x，不见任何结构参数。

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

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

  infix 20 _∈ᵗ_

传递类

载体上的类 M，若成员的成员仍在其中，称为传递。绝对性一章的诸定理消费的恰是这一前提，第四部的世界也由传递的阶段砌成；名字在此铸下，与它谈论的成员关系为邻。

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

子结构

↾ 读作「限制」：教科书里从全宇宙过渡到 $(A, \in \restriction A)$ 的那一步。给定命题值的类 M，限制结构 𝒮 ↾ M 以「元素配上属于 M 的证明」的对为载体，两个关系沿第一投影继承。值得品味的后果是：在 𝒮 ↾ M 上实例化整个框架，语法的常量域就自动只含 M 的成员。「参数只能来自这个类」不再是需要巡查的附加条件，而成为类型的形状；第四部正是经由这条通道构造可构造宇宙。

_↾_ : ∀ {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ))
    → (ZFStructure.S 𝒮 → hProp ℓ) → ZFStructure (hPropAlgebra ℓ)
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∈ S ] (x ∈ᶜ M)
  ; isSetS = isSetΣSndProp isSetS (λ x → (M x) .snd)
  ; _≈ˢ_   = λ a b → fst a ≈ˢ fst b
  ; _∈ˢ_   = λ a b → fst a ∈ˢ fst b }
  where open ZFStructure 𝒮

infixl 21 _↾_

限制结构的等词比较底层元素；由于隶属命题值的类无关乎证明，第一投影的相等可反射回对的相等，毫无损失。

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

小结

结构就是三个投影：载体、等词、成员，取值于真值代数，不带公理；传递类为后文各章反复消费的条件命名；↾ 把结构裁剪到一个类而毫无损失 (↾-reflects)。一边是语法，一边是结构：下一章让它们相遇。