可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

module L.Coding.EnvironmentSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

给定可构造集合 B 与自然数 n，本章构造 L 的元素 envSet n，其元素恰为取值于 B 的长度 n 环境。

写下十条子句的那一章说了「单个东西是某集合之上的环境」是什么意思，却把「它们全体是否构成一个集合」这个问题推开了。本章回答它：满足关系的谓词将从这个共同的环境集合中分离出来。

这里使用的是诸公理已经给出的路线。给定一个长度，所有取值落在 L 的某个集合中的环境由一个小类型索引；每个环境都是 L 的元素，因此它们全都位于某个共同层之下。再按相应描述从该层中分离，所得集合恰好包含这些环境。此处不需要替换，也不需要递归。

open import Cubical.Data.FinData using ( inj-toℕ )

open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈∈ₛ; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropView 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

小族之下的一层

stageFor 找到一个包含任意可构造集合小族所有元素的序数层，从而提供分离所需的共同外围层。

它做的正是 smallDom 所做的事，但把那个序数保留下来而不隐藏，因为此处需要的是一条关于层、而非关于模型某集合的引理。

stageFor : (X : Type ℓ) (f : X → S)
         → Σ[ β ∶ V ℓ ] (IsOrd β × ((x : X) → ⟨ (f x) .fst ∈ Lset β ⟩))
stageFor X f = β , (oβ , mem)
  where
  b = boundingOrd X (λ x → stage ((f x) .fst) (f x .snd))
        (λ x → stage-ord ((f x) .fst) (f x .snd))
  β = b .fst
  oβ : IsOrd β
  oβ = b .snd .fst
  mem : (x : X) → ⟨ (f x) .fst ∈ Lset β ⟩
  mem x = Lset-mono {α = β} {β = stage ((f x) .fst) (f x .snd)} (b .snd .snd x)
            (stage-mem ((f x) .fst) (f x .snd))

单个环境，作为模型的元素

对每个 g : Fin n → ⟪ B ⟫，envSL 证明其有穷图可构造，因此封装后的 envS g 可由 stageFor 定界。

落在 L 的某集合之上的环境是由「数码与元素」之对组成的有穷集；而 L 之元素的元素仍是 L 的元素，故这些对也是，于是前一条层引理恰好适用于此。

module _ (B : S) where

private
  ix : ⟪ B .fst ⟫ → S
  ix m = ⟪ B .fst ⟫↪ m
       , isL-trans (∈∈ₛ {a = ⟪ B .fst ⟫↪ m} {b = B .fst} .snd (∈ₛ⟪ B .fst ⟫↪ m))
           (B .snd)

Ix : ℕ → Type ℓ
Ix n = Fin n → ⟪ B .fst ⟫

opaque
  envSL : {n : ℕ} (g : Ix n) → ⟨ isL (env (λ i → (ix (g i)) .fst)) ⟩
  envSL {n} g = envL β oβ (λ i → (ix (g i)) .fst) mem
    where
    pairs : Lift {ℓ-zero} {ℓ} (Fin n) → S
    pairs i = prʟ (numeralL (toℕ (lower i))) (ix (g (lower i)))

    sf : Σ[ b ∶ V ℓ ] (IsOrd b
       × ((i : Lift {ℓ-zero} {ℓ} (Fin n)) → ⟨ (pairs i) .fst ∈ Lset b ⟩))
    sf = stageFor (Lift {ℓ-zero} {ℓ} (Fin n)) pairs

    β : V ℓ
    β = sf .fst

    oβ : IsOrd β
    oβ = sf .snd .fst

    mem : (i : Fin n) → ⟨ pr (# (toℕ i)) ((ix (g i)) .fst) ∈ Lset β ⟩
    mem i = subst (λ w → ⟨ w ∈ Lset β ⟩)
      (prʟ-fst (numeralL (toℕ i)) (ix (g i))
        ∙ cong₂ pr (numeralL-fst (toℕ i)) refl)
      (sf .snd .snd (lift i))

envS : {n : ℕ} → Ix n → S
envS g = env (λ i → (ix (g i)) .fst) , envSL g

分离出环境之集

envFo n 把 envOverAt 特化到固定长度 n 与基集合 B；在共同层中的分离定义 envSet n 及其成员关系等式。

那条描述需要三个自变量，而分离只提供一个变元，故另外两个被绑定到固定的常元上。这要花三行，却让那条描述保持本章当初写下的形式，比省下这三行更值得。

private
  nn : ℕ → S
  nn k = # k , numL k

envFo : (n : ℕ) → Formula S 1
envFo n = ∃̇ (∃̇ ( (var (suc zero) ≐ con (nn n))
               ∧̇ ((var zero ≐ con B)
               ∧̇ envOverAt (suc (suc zero)) (suc zero) zero) ))

private
  sf : (n : ℕ) → Σ[ β ∶ V ℓ ] (IsOrd β × ((g : Ix n) → ⟨ (envS g) .fst ∈ Lset β ⟩))
  sf n = stageFor (Ix n) envS

  amb : (n : ℕ) → S
  amb n = LsetS (sf n .fst) (sf n .snd .fst)

opaque
  envSet : (n : ℕ) → S
  envSet n = hasSeparationL (amb n) (envFo n) .fst .fst

  envSet-mem : (n : ℕ) (x : S)
             → (x ∈ˢ envSet n) ≡ ((x ∈ˢ amb n) ⊓ ((x ∷ []) ⊨ envFo n))
  envSet-mem n = hasSeparationL (amb n) (envFo n) .fst .snd

每个环境都在其中

对 g : Fin n → ⟪ B ⟫，证明的核心是核对其图为单值、定义域为 n，且恰含所需的值与有序对，因而属于 envSet n。

四个合取项，而每一条都只是把那条描述对着「环境究竟是什么」读一遍。单值性与那两条包含关系直接由成员关系规格得出，而后者是 refl；只有定义域那一条需要算术，因为「定义域是数码 n」说的正是「n 以下的诸序号恰是 n 以下的诸数码」。

module _ {n : ℕ} (g : Ix n) where

private
  out : (s : V ℓ) → ⟨ s ∈ (envS g) .fst ⟩
      → ∥ (Σ[ i ∶ Fin n ] (pr (# (toℕ i)) ((ix (g i)) .fst) ≡ s)) ∥₁
  out s = map₁ (λ { (li , e) → lower li , e })

  into : (i : Fin n) → ⟨ pr (# (toℕ i)) ((ix (g i)) .fst) ∈ (envS g) .fst ⟩
  into i = ∣ lift i , refl ∣₁

  val∈ : (i : Fin n) → ⟨ (ix (g i)) .fst ∈ B .fst ⟩
  val∈ i = ∈∈ₛ {a = ⟪ B .fst ⟫↪ (g i)} {b = B .fst} .snd (∈ₛ⟪ B .fst ⟫↪ (g i))

  δ : Vec S 3
  δ = B ∷ nn n ∷ envS g ∷ []

  E : Fin 3
  E = suc (suc zero)

envOver : ⟨ δ ⊨ envOverAt E (suc zero) zero ⟩
envOver = sv , (dom , (vals , pairs))
  where
  sv : ⟨ δ ⊨ svAt E ⟩
  sv = svAt-in E δ (λ x y y' p q →
    rec₁ (setIsSet (y .fst) (y' .fst))
      (λ { (i , ei) → rec₁ (setIsSet (y .fst) (y' .fst))
        (λ { (j , ej) → sym (pr-inj ei .snd)
           ∙ cong (λ k → (ix (g k)) .fst)
               (inj-toℕ (#-inj′ (pr-inj ei .fst ∙ sym (pr-inj ej .fst))))
           ∙ pr-inj ej .snd })
        (out (pr (x .fst) (y' .fst)) q) })
      (out (pr (x .fst) (y .fst)) p))

  dom : ⟨ δ ⊨ domAt E (suc zero) ⟩
  dom x = fwd , bwd
    where
    fwd : ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩ → ⟨ x .fst ∈ (# n) ⟩
    fwd hd = rec₁ ((x .fst ∈ (# n)) .snd)
      (λ { (y , p) → rec₁ ((x .fst ∈ (# n)) .snd)
        (λ { (i , ei) → subst (λ w → ⟨ w ∈ (# n) ⟩) (pr-inj ei .fst)
               (#mono (toℕ i) n (toℕ<n i)) })
        (out (pr (x .fst) (y .fst)) p) })
      (subst ⟨_⟩ (inDomAt-adequate (suc E) zero (x ∷ δ)) hd)

    bwd : ⟨ x .fst ∈ (# n) ⟩ → ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩
    bwd hx = subst ⟨_⟩ (sym (inDomAt-adequate (suc E) zero (x ∷ δ)))
      (map₁
        (λ { (m , m<n , e) →
          ix (g (fromℕ' n m m<n))
          , subst (λ w → ⟨ pr w ((ix (g (fromℕ' n m m<n))) .fst)
                             ∈ (envS g) .fst ⟩)
              (cong #_ (toFromId' n m m<n) ∙ sym e) (into (fromℕ' n m m<n)) })
        (∈#-elim n (x .fst) hx))

  vals : ⟨ δ ⊨ valuesInAt E zero ⟩
  vals x y hp = rec₁ ((y .fst ∈ B .fst) .snd)
    (λ { (i , ei) → subst (λ w → ⟨ w ∈ B .fst ⟩) (pr-inj ei .snd) (val∈ i) })
    (out (pr (x .fst) (y .fst))
      (subst ⟨_⟩ (appAt-adequate (suc (suc E)) (suc zero) zero (y ∷ x ∷ δ))
        hp))

  pairs : ⟨ δ ⊨ pairsInAt E (suc zero) zero ⟩
  pairs = pairsIn-in E (suc zero) zero δ
    (λ s s∈ → map₁
      (λ { (i , ei) → nn (toℕ i)
         , ( ix (g i)
           , ( #mono (toℕ i) n (toℕ<n i) , (val∈ i , sym ei) ) ) })
      (out (s .fst) s∈))

envSetIn : ⟨ (envS g ∷ []) ⊨ envFo n ⟩
envSetIn = ∣ nn n , ∣ B , (refl , (refl , envOver)) ∣₁ ∣₁

从元素恢复环境

反过来，元素 x 满足的四条 envOverAt 子句确定函数 g : Fin n → ⟪ B ⟫，外延性再把 x 与 envS g 等同起来。

另一个方向也是四条子句从环境中读出被绑定变元时所需的；另有七条子句以较弱的形式使用它：子句绑定自己的周遭集合，只断言其元素恰为这些环境，因此使用该子句时必须把这项描述识别为这个集合。两种用途来自同一个恢复过程。这也解释了为何环境和三个槽位作为参数给出，而不固定为特定对象：各子句可以把它们放在自身框架要求的位置。满足该描述的集合是一个函数图。恢复这个函数是四个合取项唯一需要共同作用之处：定义域条件说明长度以下的每个序号都有条目，单值性说明条目至多一个，所以「该条目存在」是命题，可以消去定义域条件给出的截断。随后由成员关系取得索引；这里无需截断，因为集合自身索引的纤维本来就是不截断的。

外延性补全证明：一个方向来自诸条目，另一个来自「由诸对构成」那一条，而若缺了那一条，不需要的元素就会混进来。

module Recover (n : ℕ) {k : ℕ} (γ : Vec S k) (Ei di bi : Fin k)
  (qd : (lookup di γ) .fst ≡ # n) (qb : (lookup bi γ) .fst ≡ B .fst)
  (h : ⟨ γ ⊨ envOverAt Ei di bi ⟩)
  where

private
  e : S
  e = lookup Ei γ

  Entry : Fin n → Type (ℓ-suc ℓ)
  Entry i = Σ[ y ∶ S ] ⟨ pr (# (toℕ i)) (y .fst) ∈ e .fst ⟩

  isPropEntry : (i : Fin n) → isProp (Entry i)
  isPropEntry i (y , p) (y' , p') =
    Σ≡Prop (λ w → (pr (# (toℕ i)) (w .fst) ∈ e .fst) .snd)
      (Σ≡Prop (λ v → (isL v) .snd)
        (svAt-out Ei γ (envOver-sv Ei di bi γ h)
          (nn (toℕ i)) y y' p p'))

  entry : (i : Fin n) → Entry i
  entry i = rec₁ (isPropEntry i) (λ z → z)
    (domAt-in Ei di γ (envOver-dom Ei di bi γ h)
      (nn (toℕ i)) (subst (λ z → ⟨ (# (toℕ i)) ∈ z ⟩) (sym qd)
        (#mono (toℕ i) n (toℕ<n i))))

  fib : (i : Fin n) → Σ[ m ∶ ⟪ B .fst ⟫ ] (⟪ B .fst ⟫↪ m ≡ (entry i .fst) .fst)
  fib i = ∈-asFiber {a = (entry i .fst) .fst} {b = B .fst}
    (subst (λ z → ⟨ (entry i .fst) .fst ∈ z ⟩) qb
      (valuesInAt-out Ei bi γ (envOver-values Ei di bi γ h)
        (nn (toℕ i)) (entry i .fst) (entry i .snd)))

g : Ix n
g i = fib i .fst

private
  val≡ : (i : Fin n) → (ix (g i)) .fst ≡ (entry i .fst) .fst
  val≡ i = fib i .snd

  fwd : (w : V ℓ) → ⟨ w ∈ (envS g) .fst ⟩ → ⟨ w ∈ e .fst ⟩
  fwd w = rec₁ ((w ∈ e .fst) .snd)
    (λ { (li , q) → subst (λ z → ⟨ z ∈ e .fst ⟩)
           (cong (pr (# (toℕ (lower li)))) (sym (val≡ (lower li))) ∙ q)
           (entry (lower li) .snd) })

  bwd : (w : V ℓ) → ⟨ w ∈ e .fst ⟩ → ⟨ w ∈ (envS g) .fst ⟩
  bwd w hw = rec₁ squash₁
    (λ { (u , (v , (u∈ , (v∈ , eq)))) → rec₁ squash₁
      (λ { (m , (m<n , um)) →
        let i = fromℕ' n m m<n
            iu : # (toℕ i) ≡ u .fst
            iu = cong #_ (toFromId' n m m<n) ∙ sym um
            hv : ⟨ pr (# (toℕ i)) (v .fst) ∈ e .fst ⟩
            hv = subst (λ z → ⟨ z ∈ e .fst ⟩)
                   (eq ∙ cong (λ z → pr z (v .fst)) (sym iu)) hw
            same : v .fst ≡ (entry i .fst) .fst
            same = svAt-out Ei γ (envOver-sv Ei di bi γ h)
                     (nn (toℕ i)) v (entry i .fst) hv (entry i .snd)
        in ∣ lift i , cong (pr (# (toℕ i))) (val≡ i ∙ sym same)
                    ∙ cong (λ z → pr z (v .fst)) iu ∙ sym eq ∣₁ })
      (∈#-elim n (u .fst) (subst (λ z → ⟨ u .fst ∈ z ⟩) qd u∈)) })
    (pairsIn-out Ei di bi γ
      (envOver-pairs Ei di bi γ h)
      (w , isL-trans {x = e .fst} {y = w} hw (e .snd)) hw)

recovers : e .fst ≡ (envS g) .fst
recovers = extensionalV (λ w → ⇔toPath (bwd w) (fwd w))

envSet-in : {n : ℕ} (g : Ix n) → ⟨ envS g ∈ˢ envSet n ⟩
envSet-in {n} g = subst ⟨_⟩ (sym (envSet-mem n (envS g)))
  (sf n .snd .snd g , envSetIn g)

envSet-out : (n : ℕ) (x : S) → ⟨ x ∈ˢ envSet n ⟩
           → ∥ (Σ[ g ∶ Ix n ] (x .fst ≡ (envS g) .fst)) ∥₁
envSet-out n x hx = rec₁ squash₁
  (λ { (d , hd) → map₁
    (λ { (b , (qd , (qb , hov))) →
      Recover.g n (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero qd qb hov
      , Recover.recovers n (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero
          qd qb hov })
    hd })
  (subst ⟨_⟩ (envSet-mem n x) hx .snd)

小结

两个方向刻画了 envSet n：属于该集合等价于它是取值于 B 的长度 n 赋值图，因此后面的构造能在 L 内量化环境。

envSet 是诸负子句取补集所在的那个周遭集合，而它双向可读：envSet-in 把载体之上的每个环境放进去，envSet-out 从任一元素恢复出「它是其图」的那个函数。后者正是四条子句在从环境读出被绑变元时所要的，也是唯一需要那条描述的四个合取项协同上阵的一条。

这里记录两次测量，第二次把本书已有的一条规则说得更精确。把环境固定为具体值后证明第四个合取项，十分钟仍未完成；先在环境为变元时证明同一引理，再将其应用，耗时则几乎无法测出。沿充分性等式替换满足关系时，替换必须发生在自变量仍是变元之处；若写在具体元素上，归一化会展开整套绝对性结果以及这些元素的可构造性证书。只在构造处封装证书仍不足以避免这一点。恢复部分采用同样的写法：那条描述的两个常元槽保留为由等式约束的参数，而不固定为具体对象，因此不会在具体环境的满足关系之下发生替换。

定长环境之集

小族之下的一层

单个环境，作为模型的元素

分离出环境之集

每个环境都在其中

从元素恢复环境

小结