Smallness

上一章以一句宇宙警告收尾：V ℓ 是由小索引数据造出的大类型，其真值住在高一层的 hProp (ℓ-suc ℓ)。这句警告的分量在于：库提供的每一件造集装置，头一件就是 sett，都只收小输入：小索引类型、小谓词。要想用一条性质造出集合，先得把这条性质的真值降下一个宇宙。本章打造的正是这套工具，而它的回报是本部第一条值得裱起来的定理：Δ₀ 公式的分离不花任何公理。

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

open import Base.Prelude
open import Base.Truth

module V.Smallness {ℓ : Level} where

open import Base.Impredicativity using ( isSmall )
open import FOL.ZFStructure using ( ZFStructure; _↾_ )
open import FOL.Syntax
  using ( Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy
  using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-¬; δ-⊤; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; secEq; propBiimpl→Equiv )
import Cubical.Functions.Logic as Logic
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Sum as Sum
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∼_; identityPrinciple; _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module SeparationSet )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open ZFStructure 𝒮ᵥ

何谓小

高一层的命题是小的，指它与某个低一层的命题等价：这个定义 (isSmall) 铸于第零部，在那里，降层接口把它一揽子断言于每个命题。本章不作这种假设。它逐原子地挣得实例，而整章无非是把挣来的见证传来传去的一套体操。

原子的小性直接来自库。这就是上一章瞥见过的局部小性装置：成员关系有小孪生 ∈ₛ (∈∈ₛ 双向换形)，集合相等经 identityPrinciple 压缩为双相似 ∼。

small-∈ : (a b : S) → isSmall (a ∈ˢ b)
small-∈ a b = (a ∈ₛ b) ,
  propBiimpl→Equiv (snd (a ∈ˢ b)) (snd (a ∈ₛ b))
    (∈∈ₛ {a = a} {b = b} .fst) (∈∈ₛ {a = a} {b = b} .snd)

small-≡ : (a b : S) → isSmall (a ≈ˢ b)
small-≡ a b = (a ∼ b) , invEquiv identityPrinciple

联结词保小

六个命题运算逐个传递小性见证，每条证明都是双蕴含的机械搬运。(限定名 Logic 是库在低一层的联结词，即压缩的落点。)

small⊓ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊓ Q)
small⊓ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⊓ Q') ,
  propBiimpl→Equiv (snd (P ⊓ Q)) (snd (P' Logic.⊓ Q'))
    (λ pq → equivFun eP (pq .fst) , equivFun eQ (pq .snd))
    (λ pq → invEq eP (pq .fst) , invEq eQ (pq .snd))

small⊔ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊔ Q)
small⊔ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⊔ Q') ,
  propBiimpl→Equiv (snd (P ⊔ Q)) (snd (P' Logic.⊔ Q'))
    (PT.map (Sum.map (equivFun eP) (equivFun eQ)))
    (PT.map (Sum.map (invEq eP) (invEq eQ)))

small⇒ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⇒ Q)
small⇒ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⇒ Q') ,
  propBiimpl→Equiv (snd (P ⇒ Q)) (snd (P' Logic.⇒ Q'))
    (λ f p' → equivFun eQ (f (invEq eP p')))
    (λ g p → invEq eQ (g (equivFun eP p)))

small¬ : {P : hProp (ℓ-suc ℓ)} → isSmall P → isSmall (¬ P)
small¬ {P} (P' , eP) = (Logic.¬ P') ,
  propBiimpl→Equiv (snd (¬ P)) (snd (Logic.¬ P'))
    (λ np p' → np (invEq eP p'))
    (λ np' p → np' (equivFun eP p))

small⊤ : isSmall ⊤
small⊤ = Logic.⊤ ,
  propBiimpl→Equiv (⊤ .snd) (snd (Logic.⊤ {ℓ}))
    (λ _ → tt*) (λ _ → tt*)

small⊥ : isSmall ⊥
small⊥ = (⊥* , isProp⊥*) ,
  propBiimpl→Equiv isProp⊥* isProp⊥* (λ ()) (λ ())

有界量词保小

承重的一步到了，语法章最古老的那句许诺，在此以宇宙为通货兑付。范围取全 V ℓ 的量词量化在大类型上，没有任何理由是小的。而以集合 a 为界的量词可以改在库的小成员类型 ⟪ a ⟫ 上量化，即 a 的族的索引类型，小性就此存活。往返两趟走 ∈-asFiber，其纤维不加截断，因为 ⟪ a ⟫↪ 是嵌入：从「a 的成员」回到「⟪ a ⟫ 的索引」是函数，不是选择。

small-∀∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (⋀ S (λ x → (x ∈ˢ a) ⇒ B x))
small-∀∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋀ S (λ x → (x ∈ˢ a) ⇒ B x)
  Qsm = Logic.∀[]-syntax (λ (m : ⟪ a ⟫) → sm (⟪ a ⟫↪ m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd f m = equivFun (sm (⟪ a ⟫↪ m) .snd)
                     (f (⟪ a ⟫↪ m) (∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)))
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd g x x∈a =
    subst (λ v → ⟨ B v ⟩) (mf .snd)
          (invEq (sm (⟪ a ⟫↪ (mf .fst)) .snd) (g (mf .fst)))
    where mf = ∈-asFiber {a = x} {b = a} x∈a

small-∃∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (⋁ S (λ x → (x ∈ˢ a) ⊓ B x))
small-∃∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋁ S (λ x → (x ∈ˢ a) ⊓ B x)
  Qsm = Logic.∃[]-syntax (λ (m : ⟪ a ⟫) → sm (⟪ a ⟫↪ m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd = PT.map λ where
    (x , x∈a , bx) →
      let mf = ∈-asFiber {a = x} {b = a} x∈a
      in mf .fst ,
         equivFun (sm (⟪ a ⟫↪ (mf .fst)) .snd)
                  (subst (λ v → ⟨ B v ⟩) (sym (mf .snd)) bx)
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd = PT.map λ where
    (m , q) → ⟪ a ⟫↪ m , ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)
            , invEq (sm (⟪ a ⟫↪ m) .snd) q

分离的水管

小性买到的东西：逐点小的谓词可以分离。库的 SeparationSet 只收小谓词，小性见证恰好是入场券；规格以模型 record 的字段形状交还。本部往后的每一次分离，无论小性由谁买单，都流经这一根水管。

separateFromSmall : (a : S) (P : S → hProp (ℓ-suc ℓ))
                  → (∀ y → isSmall (P y))
                  → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y))
separateFromSmall a P sm = Sep.SEPAREE , λ y → ⇔toPath (fwd y) (bwd y)
  where
  ϕₛ : S → hProp ℓ
  ϕₛ y = sm y .fst
  module Sep = SeparationSet a ϕₛ
  fwd : ∀ y → ⟨ y ∈ˢ Sep.SEPAREE ⟩ → ⟨ (y ∈ˢ a) ⊓ P y ⟩
  fwd y y∈s = ∈∈ₛ {a = y} {b = a} .snd (Sep.separation-ax y .fst y∈ₛs .fst)
            , invEq (sm y .snd) (Sep.separation-ax y .fst y∈ₛs .snd)
    where y∈ₛs = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .fst y∈s
  bwd : ∀ y → ⟨ (y ∈ˢ a) ⊓ P y ⟩ → ⟨ y ∈ˢ Sep.SEPAREE ⟩
  bwd y yp = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .snd (Sep.separation-ax y .snd
               (∈∈ₛ {a = y} {b = a} .fst (yp .fst) , equivFun (sm y .snd) (yp .snd)))

Δ₀ 公式求值小

Δ₀ 见证开始挣第二份薪水。对 Δ₀ 见证做一次归纳，即知带见证的公式在任何环境下的真值都小：两个原子情形是库压缩，八个联结词情形是封闭性引理，两个有界量词情形消费 small-∀∈ 与 small-∃∈。没有无界量词的情形，因为见证压根没有那两个构造子：缺席即分类。这是压在 Δ₀ 见证上的第二条承重归纳 (第一条是绝对性)，也是 Lévy 层级兼任成本账簿的原因：Δ₀ 意谓免费，在宇宙层级的精确意义上。

module SemanticsV = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ
open SemanticsV using ( _^_ )

module Δ₀Small {ℓc} {K : Type ℓc} (ι : K → S) where

  open SemanticsV.At K ι

  Δ₀-small : ∀ {n} {φ : Formula K n} → Δ₀ φ → (γ : S ^ n) → isSmall (γ ⊨ φ)
  Δ₀-small (δ-∈ {t = t} {u}) γ = small-∈ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-≐ {t = t} {u}) γ = small-≡ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-∧ {φ = φ} {ψ} c d) γ =
    small⊓ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-∨ {φ = φ} {ψ} c d) γ =
    small⊔ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-⇒ {φ = φ} {ψ} c d) γ =
    small⇒ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-¬ {φ = φ} c) γ = small¬ {P = γ ⊨ φ} (Δ₀-small c γ)
  Δ₀-small δ-⊤ γ = small⊤
  Δ₀-small δ-⊥ γ = small⊥
  Δ₀-small (δ-∀∈ {t = t} {φ = φ} c) γ =
    small-∀∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))
  Δ₀-small (δ-∃∈ {t = t} {φ = φ} c) γ =
    small-∃∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))

定理：Δ₀ 分离免费

把这条归纳与那根水管在典范常量解释处一复合，招牌定理应声落地：携带 Δ₀ 见证的公式，其分离不需任何降层、不花任何公理，一路 --safe。模型章仍欠全分离，但这条定理是一个贯穿主题的第一份硬证据：Δ₀ 见证是可携资产，随身携带自有回报。

open Δ₀Small id
open SemanticsV.At S id using ( _⊨_ )

separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ
           → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ)))
separateΔ₀ a φ c = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → Δ₀-small c (y ∷ []))

本质小的世界

小性还有一种买法，买单的不是 Δ₀ 见证而是地段。当量化范围自身等价于某个小类型时，连无界量词也保小：沿等价搬运量化即可。这与上文的成本账簿并不冲突，那里标价的是范围为全 V ℓ 的量词；此处的范围是限制结构 𝒮ᵥ ↾ M 的载体，小性恰是「限制」二字买来的。

small-⋀ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (⋀ A B)
small-⋀ {A} {X} e {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋀ A B
  Qsm = Logic.∀[]-syntax (λ (m : X) → sm (equivFun e m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd f m = equivFun (sm (equivFun e m) .snd) (f (equivFun e m))
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd g a = subst (λ v → ⟨ B v ⟩) (secEq e a)
                  (invEq (sm (equivFun e (invEq e a)) .snd) (g (invEq e a)))

small-⋁ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (⋁ A B)
small-⋁ {A} {X} e {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋁ A B
  Qsm = Logic.∃[]-syntax (λ (m : X) → sm (equivFun e m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd = PT.map λ where
    (a , ba) → invEq e a ,
               equivFun (sm (equivFun e (invEq e a)) .snd)
                        (subst (λ v → ⟨ B v ⟩) (sym (secEq e a)) ba)
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd = PT.map λ where
    (m , q) → equivFun e m , invEq (sm (equivFun e m) .snd) q

后果是：在本质小的限制结构上，任何公式求值皆小，无需 Δ₀ 见证。量词子句沿等价行走，原子经第一投影落回 V 的原子小性。这就是「在小世界里说话，说什么都小」，也是第四部那一步构造的发动机。

module InnerSmall (M : S → hProp (ℓ-suc ℓ))
                  (X : Type ℓ) (e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M)))
                  {ℓc} {K : Type ℓc}
                  (ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)) where

  SM : Type (ℓ-suc ℓ)
  SM = Σ[ x ∈ S ] (x ∈ᶜ M)

  𝒮M : ZFStructure (hPropAlgebra (ℓ-suc ℓ))
  𝒮M = 𝒮ᵥ ↾ M

  module SemanticsM = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮M
  open SemanticsM.At K ι renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) public

  ⊨ᵐ-small : ∀ {n} (φ : Formula K n) (δ : SM ^ n) → isSmall (δ ⊨ᵐ φ)
  ⊨ᵐ-small (t ∈̇ u)  δ = small-∈ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (t ≐ u)  δ = small-≡ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (φ ∧̇ ψ)  δ =
    small⊓ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (φ ∨̇ ψ)  δ =
    small⊔ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (φ ⇒̇ ψ)  δ =
    small⇒ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (¬̇ φ)    δ = small¬ {P = δ ⊨ᵐ φ} (⊨ᵐ-small φ δ)
  ⊨ᵐ-small ⊤̇        δ = small⊤
  ⊨ᵐ-small ⊥̇        δ = small⊥
  ⊨ᵐ-small (∃̇ φ)    δ =
    small-⋁ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇ φ)    δ =
    small-⋀ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇∈ t φ) δ =
    small-⋀ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⇒ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
      small⇒ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))
  ⊨ᵐ-small (∃̇∈ t φ) δ =
    small-⋁ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⊓ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
      small⊓ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))

小结

小性即与低一层命题的等价 (isSmall)；原子经库压缩，联结词与有界量词传递小性见证，separateFromSmall 是从小谓词到集合的唯一水管。归纳 Δ₀-small 让 Lévy 层级兼任成本账簿，separateΔ₀ 是其中的免费档。Δ₀ 够不到的部分在模型章标价，而那个价格有名字：降层。