集合的可定义子集

M : S → hProp (ℓ-suc ℓ)
M x = x ∈ˢ A

e : ⟪ A ⟫ ≃ (Σ[ x ∶ S ] (x ∈ᶜ M))
e = compEquiv (invEquiv (presentation A))

于是常元解释 ι 就是把等价 e 当作函数来读。由于公式的常元域将取 ⟪ A ⟫ 本身，语言中的一个常元就是 A 的某个元素的索引，ι 把它解码到限制载体中。ι m 的第一投影按定义就是底层集合 ⟪ A ⟫↪ m，成员关系证明会不加修饰地使用这一事实。

      (Σ-cong-equiv-snd (λ v →
        propBiimpl→Equiv ((v ∈ₛ A) .snd) ((v ∈ˢ A) .snd)
          (∈∈ₛ {a = v} {b = A} .snd) (∈∈ₛ {a = v} {b = A} .fst)))

ι : ⟪ A ⟫ → Σ[ x ∶ S ] (x ∈ᶜ M)
ι = equivFun e

在这些数据上开启 InnerSmall 便重建了世界：限制到「属于 A」的结构 𝒮M、其满足关系 ⊨ᵐ，以及定理 ⊨ᵐ-small，即 ⟪ A ⟫ 上的每个公式都求值为小命题。以 public 开启意味着后续章节恰在这些名字下读取内层满足。从这里起，「满足」一律指这个内层关系，量词只限于 A 的元素。

open InnerSmall M ⟪ A ⟫ e {K = ⟪ A ⟫} ι public

内层满足 ⊨ᵐ 与其小性就位后，算子可直接定义。smallSat φ m 是 φ 在元素 m 处的真值，位于低一层宇宙；defSet φ 是 φ 从 A 中定出的子集，在 φ 选中的元素上应用 sett；Def A 则是这些子集的全体，以公式自身为索引。公式是 Type ℓ 中的归纳数据，恰好构成合法的小索引；这里使用的正是语法当索引集。

压缩 smallSat 打包了两步求值：⊨ᵐ-small φ (ι m ∷ []) 是一个对子，第一分量是与内层满足陈述等价的小命题，第二分量是那个等价本身。环境 ι m ∷ [] 只有一项，因为 φ 只有一个自由变元槽位，由元素 m 经 ι 填入。与此独立地，φ 中出现的任何常元都经常元解释 ι 解释，因此可以指称 A 的任意元素：参数经由常元进入，而变元那一项只是固定单个自由槽位的求值位置。底层命题 ⟨ smallSat φ m ⟩ 表示 φ 在 (A, ∈) 内于 m 处成立，且已是适合为 sett 充当索引的小形式。

smallSat : Formula ⟪ A ⟫  → ⟪ A ⟫ → hProp ℓ
smallSat φ m = ⊨ᵐ-small φ (ι m ∷ []) .fst

defSet : Formula ⟪ A ⟫  → S
defSet φ = sett (Σ[ m ∶ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))

Def : S

可定义子集 defSet φ 由索引类型 Σ[ m ∶ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩ 呈现：一个索引是元素 m 连同「φ 在 m 处成立」的证明，索引映射把这个对子送到集合 ⟪ A ⟫↪ m。注意截断纪律：证明分量是证明而非被选取的数据，defSet φ 的元素只要求这样的证明仅仅存在。最后，Def 在上一层重复同一构造，以公式本身为索引族：每个索引仅仅命中某个 defSet φ。由于公式住在 Type ℓ 中，索引类型是小的，结果仍是层级中的集合。

Def = sett (Formula ⟪ A ⟫ ) defSet

成员关系，给出规格

Def 与每个 defSet φ 都由 sett 构造，因此其成员关系按定义表示相应索引的仅仅存在性。对 Def 无须另作证明：Def 的元素仅仅就是某个 defSet φ。可定义子集有两条规格：它的元素都属于 A；元素 ⟪ A ⟫↪ m 属于 defSet φ，当且仅当内层世界在 m 处满足 φ。这两条规格直接给出「可定义子集」的含义；smallSat 的压缩只是编码，并不改变这个等价关系。

第一条规格说每个 defSet φ 都包含于 A。defSet φ 的元素仅仅来自带某个证明的索引 (m , _)，连同把索引集合等同于 y 的路径 q。由于 A 中的成员关系是命题，截断可消入命题：该证明沿 q 把已知事实 ⟪ A ⟫↪ m ∈ˢ A 搬运过去，得到 y ∈ˢ A。这个已知事实正是小成员关系 ⟪ A ⟫↪ m ∈ₛ A 经 ∈∈ₛ 转换而来。

defSet⊆A : (φ : Formula ⟪ A ⟫ ) (y : S) → ⟨ y ∈ˢ defSet φ ⟩ → ⟨ y ∈ˢ A ⟩
defSet⊆A φ y = rec₁ ((y ∈ˢ A) .snd) λ { ((m , _) , q) →
  subst (λ v → ⟨ v ∈ˢ A ⟩) q
        (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) }

private

第二条规格是本章的核心，它被陈述为命题之间的路径，而不是一对蕴含：⟪ A ⟫↪ m 属于 defSet φ 这一命题等于内层满足陈述 (ι m ∷ []) ⊨ᵐ φ。辅助定义 decode 把 smallSat 重新展开成完整的对子，于是其第二分量中的等价对两个方向都可用。另请注意私有的单射性引理：⟪ A ⟫↪ 是从 ⟪ A ⟫ 到载体的嵌入，其值之间的路径来自索引之间的路径；这将从集合的路径恢复出 m' ≡ m。

  ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
  ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

defSet-mem : (φ : Formula ⟪ A ⟫ ) (m : ⟪ A ⟫)
           → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((ι m ∷ []) ⊨ᵐ φ)
defSet-mem φ m = ⇔toPath fwd bwd

正向展开成员关系仅仅给出的内容：索引 (m' , h)，其中 h 证明 smallSat φ m'，以及满足 ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m 的路径 q。单射性把 q 变成 m' ≡ m，沿它搬运 h 得到 smallSat φ m 的证明。然后 decode 的第二分量，即小命题与内层满足之间的等价，把这个证明转换为目标陈述。每个部件都派上用场：截断给出索引，嵌入给出索引间的路径，移送搬运证明，等价将其解码。

  where
  decode = ⊨ᵐ-small φ (ι m ∷ [])
  fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩ → ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩
  fwd = rec₁ (((ι m ∷ []) ⊨ᵐ φ) .snd) λ { ((m' , h) , q) →
    invEq (decode .snd) (subst (λ k → ⟨ smallSat φ k ⟩) (⟪⟫↪-inj q) h) }

反向很短，因为等价同样可以反向运行：给定 hφ : (ι m ∷ []) ⊨ᵐ φ，应用该等价得到 smallSat φ m 的证明，取索引 (m , 证明) 与平凡路径 refl。结果用 ∣_∣₁ 截断，这正是成员关系所要求的。两个方向合起来给出内层满足与可定义子集成员关系之间的精确对应。

  bwd : ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩
  bwd hφ = ∣ (m , equivFun (decode .snd) hφ) , refl ∣₁

Def 只精化，不缩水

在不假设传递性时，两条事实已经确定 Def A 的位置。恒真公式定义出整个 A，所以 A 本身是 Def A 的一个元素；而 Def A 的每个元素都是 A 的子集。这里尚未断言 A ⊆ Def A。下一节将在传递性前提下逐一可定义 A 的元素，从而证明这条更强的包含。

私有辅助 A-mem 把大的成员关系证明转成纤维形式：A 的元素 y 仅仅来自某个索引 m，满足 ⟪ A ⟫↪ m ≡ y；由于 ∈-asFiber 以数据形式返回纤维 (截断位于它消费的成员关系证明之内)，可以用 let 把对子拆开。两个集合的相等由 extensionality 证明，因此只需给出两个方向的包含。

private
  A-mem : (y : S) → ⟨ y ∈ˢ A ⟩ → Σ[ m ∶ ⟪ A ⟫ ] (⟪ A ⟫↪ m ≡ y)
  A-mem y y∈ = ∈-asFiber {a = y} {b = A} y∈

defSet⊤≡A : defSet ⊤̇ ≡ A
defSet⊤≡A = extensionality (defSet ⊤̇) A (sub₁ , sub₂)

容易的方向复用刚证得的包含。defSet ⊤̇ 的集合论元素 y 经 sett 成员关系的定义给出截断的索引；defSet⊆A 随即把 y 放进 A，转换 ∈∈ₛ 再把陈述包装成包含 ⊆ 所期望的形式。这一半完全不用 ⊤̇ 的含义：它对每个 defSet φ 都成立。

  where
  sub₁ : ⟨ defSet ⊤̇ ⊆ A ⟩
  sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = A} .fst
    (defSet⊆A ⊤̇ y (∈∈ₛ {a = y} {b = defSet ⊤̇} .snd y∈ₛ))
  sub₂ : ⟨ A ⊆ defSet ⊤̇ ⟩

反向用到「真」的含义：由于 ⊤̇ 在每个元素处成立，defSet-mem ⊤̇ m 把 ⟪ A ⟫↪ m ∈ˢ defSet ⊤̇ 等同于一个任何元素都能证明的命题，这里以恒等函数给出。于是 A 的每个元素 y，既然仅仅是 ⟪ A ⟫↪ m，就沿纤维路径被搬运进 defSet ⊤̇。注意 subst ⟨_⟩ 中 sym (defSet-mem ⊤̇ m) 的用法：该定理是命题之间的路径，因此可以按目标需要的方向搬运证明。

  sub₂ y y∈ₛ =
    let (m , q) = A-mem y (∈∈ₛ {a = y} {b = A} .snd y∈ₛ)
    in subst (λ v → ⟨ v ∈ₛ defSet ⊤̇ ⟩) q
         (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet ⊤̇} .fst
           (subst ⟨_⟩ (sym (defSet-mem ⊤̇ m)) (λ z → z)))

对偶的包含 Def∋⊆A 说 Def A 的每个元素都是 A 的子集。它的前提本身就是截断：x 仅仅是某个 defSet φ。目标是由命题经乘积构成的命题，因此 rec₁ 可以消去截断；随后沿把 x 等同于 defSet φ 的路径反向搬运 y ∈ˢ x，并应用 defSet φ 的包含。与给出 A ∈ Def 的 defSet⊤≡A 合观，图景完整：Def 把 A 作为元素包含在内，且只包含 A 的子集。

Def∋⊆A : (x : S) → ⟨ x ∈ˢ Def ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
Def∋⊆A x = rec₁ (isPropΠ λ y → isPropΠ λ _ → (y ∈ˢ A) .snd)
  (λ { (φ , q) y y∈x → defSet⊆A φ y (subst (λ s → ⟨ y ∈ˢ s ⟩) (sym q) y∈x) })

传递性之下，A ⊆ Def A

当 A 传递时，A 的每个元素 a 自身也可定义：仍用模型章构造交集的那条两符号途径，即原子公式「该变元属于 a」。分离暗含的「属于 A」条件恰好由传递性保证：a 的元素已是 A 的元素，于是原子公式刻出的正是 a。故 A ⊆ Def A：没有任何元素被遗漏。与上一节合观，迭代 Def 只增不减，正合可构造塔的需要。

子模块以 A 的传递性为显式前提。原子公式 atom mₐ 是 var zero ∈̇ con mₐ：一个自由变元槽位，加上命名元素 mₐ 的单个常元。这里再次体现了以 ⟪ A ⟫ 为常元域这一设计选择的好处：A 的每个元素都可充作常元，由 ι 解码到限制载体。

module Refine (Atrans : hPropView.Transitive 𝒮ᵥ M) where

atom : ⟪ A ⟫ → Formula ⟪ A ⟫ 
atom mₐ = var zero ∈̇ con mₐ

atom-mem : (mₐ m : ⟪ A ⟫)
         → (⟪ A ⟫↪ m ∈ˢ defSet (atom mₐ)) ≡ (⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ)

atom-mem mₐ m = defSet-mem (atom mₐ) m

defSet-atom≡ : (mₐ : ⟪ A ⟫) → defSet (atom mₐ) ≡ ⟪ A ⟫↪ mₐ
defSet-atom≡ mₐ = extensionality (defSet (atom mₐ)) (⟪ A ⟫↪ mₐ) (sub₁ , sub₂)
  where
  sub₁ : ⟨ defSet (atom mₐ) ⊆ ⟪ A ⟫↪ mₐ ⟩

  sub₁ y y∈ₛ = rec₁ ((y ∈ₛ ⟪ A ⟫↪ mₐ) .snd)
    (λ { ((m , h) , q) →
      subst (λ v → ⟨ v ∈ₛ ⟪ A ⟫↪ mₐ ⟩) q
        (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = ⟪ A ⟫↪ mₐ} .fst
          (subst ⟨_⟩ (atom-mem mₐ m) ∣ (m , h) , refl ∣₁)) })

    (∈∈ₛ {a = y} {b = defSet (atom mₐ)} .snd y∈ₛ)
  sub₂ : ⟨ ⟪ A ⟫↪ mₐ ⊆ defSet (atom mₐ) ⟩
  sub₂ y y∈ₛ =
    let y∈a     = ∈∈ₛ {a = y} {b = ⟪ A ⟫↪ mₐ} .snd y∈ₛ
        y∈A     = Atrans {x = ⟪ A ⟫↪ mₐ} {y = y} y∈a mₐ-as

        (m , q) = ∈-asFiber {a = y} {b = A} y∈A
    in subst (λ v → ⟨ v ∈ₛ defSet (atom mₐ) ⟩) q
         (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet (atom mₐ)} .fst
           (subst ⟨_⟩ (sym (atom-mem mₐ m))
             (subst (λ v → ⟨ v ∈ˢ ⟪ A ⟫↪ mₐ ⟩) (sym q) y∈a)))

    where
    mₐ-as : ⟨ ⟪ A ⟫↪ mₐ ∈ˢ A ⟩
    mₐ-as = ∈∈ₛ {a = ⟪ A ⟫↪ mₐ} {b = A} .snd (∈ₛ⟪ A ⟫↪ mₐ)

A⊆Def : (a : S) → ⟨ a ∈ˢ A ⟩ → ⟨ a ∈ˢ Def ⟩
A⊆Def a a∈ =

  let (mₐ , q) = ∈-asFiber {a = a} {b = A} a∈
  in ∣ atom mₐ , defSet-atom≡ mₐ ∙ q ∣₁

module Abs = FOL.Absoluteness.Single 𝒮ᵥ M Atrans

abs-defSet : (φ : Formula ⟪ A ⟫ ) → Δ₀ φ → (m : ⟪ A ⟫)
           → (⟪ A ⟫↪ m ∈ˢ defSet φ)
             ≡ ((⟪ A ⟫↪ m ∷ []) Abs.⊨ᵛ (mapFo ι φ))
abs-defSet φ d m =

    defSet-mem φ m
  ∙ sym (⊨-map Abs.𝒮M ι id φ (ι m ∷ []))
  ∙ Abs.abs₀ (mapΔ₀ ι d) (ι m ∷ [])