Bedrock作为集合编码图的有穷环境
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图一阶语言的满足子句谈论变元的取值，却只能对集合作量化。因此，要使满足关系能在集合论内部被计算，变元赋值本身必须先成为一个集合。本章完成这一编码：一个有穷赋值，即从变元序号到 V ℓ 中集合的函数，由它的图表示，也就是「序号的数码与该处取值」之对的集合。
这一编码的设计目标是图中的查值精确。由于键的一侧由数码构成，而数码是单射的，坐在键 i 处的那个对的第二分量恰为 i 处的值，别无他物。这条函数性命题是本章的主引理。
第二个关注点是扩张。当满足关系下降到量词之下时，新值被放在索引零处，每个旧索引上移一位；在键的一侧，这恰是 von Neumann 后继。故本章构造若干有界公式，仅凭隶属说出：一个索引是另一个的后继；一个对是把另一个的键移位后得到的；以及最终，一个集合是扩张后赋值的图。每一条都以充分性命题的形式证明：公式的满足是一条真值路径，通向关于集合的相应外部事实，而所涉的图都靠外延性逐成员比较，从不从截断的隶属数据中挑选见证。
本章的一切都在一个固定的宇宙层级 ℓ 上进行：所操作的集合是 V ℓ 的元素，语言中的公式对这些集合作量化。把层级作为显式参数，意味着整个构造可以在任何拥有该层级的地方被实例化。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Coding.Environment {ℓ : Level} where open import FOL.Syntax using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈; ⊥̇ )
本章在一阶语言的有界片段内工作：Δ₀ 公式指每个量词都以环境中的某个变元为界，故其满足只依赖于已给出的界定集合中的隶属。编码在数学上依赖两条宿主层事实：Kuratowski 对 pr 是单射的，故一个对决定其分量；数码 # n 是单射的，故一个数码决定其序号。这两条单射性合在一起，使一个赋值的图表现出函数图的行为。
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-∀∈ ) import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl; ∈sucV-elim ) open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
有界读式 prAt 在配对公式一章中已被证明是充分的，它断言给定变元槽位处的集合是另外两个槽位处的集合的 Kuratowski 对。本章直接复用其充分性引理，以及把一个分量放入对内的两条引入规则，因为移位后的条目仍是 Kuratowski 对，只是键被移动了。宿主侧使用二元和类型的地方，对应公式产生析取之处：一个值是此物或彼物，只记录取了哪一侧，不断言见证唯一。
open import L.Coding.PairFormulas {ℓ} using ( prAt; prAt-adequate; prChar-fwd; prChar-bwd ; ∈pair-introL; ∈pair-introR ) open import Cubical.Data.Unit using ( tt ) import Cubical.Data.Sum as Sum
层级中集合的隶属是一个命题，因此「图中某个条目与给定的对相关」的证明总是仅仅存在：它记录见证存在，却不把它当作普通数据提供。这种截断只能消除到取值为命题的目标中，且无法由此整体恢复出一个被选定的见证。本章凡辨认两个命题为同一，都经 ⇔toPath 完成，它把一个当且仅当变成真值之间的路径；这里的每条充分性引理都是这个形状。
open Sum using ( _⊎_; inl; inr ) import Cubical.Data.Empty as E hiding ( elim ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.Functions.Logic using ( ⇔toPath )
背景宇宙是 cubical 累积层级。集合以 sett A f 引入，即一个索引类型配一个元素族，其隶属关系与该设定中其他隶属一样是截断的。外延性原理断言：成员相同的两个集合作为路径相等。这正是比较编码图所用的工具：要证明一个候选图等于另一个，只需对每个元素证明，属于前者的命题与属于后者的命题相差一条真值路径。
open import Cubical.Data.FinData using ( toℕ; inj-toℕ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; setIsSet; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ; _⊆_; extensionality )
层级的构造给出编码所用的材料：空集、单点集、无序对 ⁅_,_⁆，以及数码。数码的递归定义是关键：# 0 是 ∅，# (suc n) 是 sucV (# n)，即 von Neumann 后继。于是「序号加一」与「键取后继」是同一个运算，这正是环境扩张能够被有界公式描述的原因。在语义一侧，真值是伴随命题性证明的命题，故公式的满足本身是一个命题，可以经一条路径与外部的集合论陈述相等同。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆; ⁅_⁆s; ∅; ∅-empty; module InfinitySet ) open InfinitySet using ( sucV; #_ ) module Sem = FOL.Semantics 𝒮ᵥ
最后，满足关系 _⊨_ 与项解释 ⟦_⟧ 取在载体 V ℓ 自身上，常元解释为恒等。于是元数为 n 的公式的环境就是真正的函数 (V ℓ) ^ n，即有穷的集合组。本章编码的是证书数据所携带的赋值，而非这个语义载体：组形式是语义求值所用的，图形式才是证书能够作为单个集合存储与操作的。
open Sem using ( _^_ ) open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )
环境的图
赋值 g : Fin n → V ℓ 成为集合 env g，其在索引 i 的键处的条目是数码 # (toℕ i) 与值 g i 的有序对。本节证明使这一表示可用的命题：lookup-spec 把「键 i 处的对属于 env g」等同于「该对的第二分量等于 g i」这一命题。
与其他层级隶属一样，env g 中的隶属是截断的；lookup-spec 的要点在于：这截断的纤维数据仍然精确地决定取值。
这一汇集是集合构造子 sett 的实例，它取一个索引类型与一个元素族。有穷索引类型 Fin n 层级低于 ℓ，故先提升；Lift 只调整宇宙，lower 取回索引。于是每个索引 li 贡献一个条目，即其序号的数码与 g 在该处的值配成的对。条目本身是普通数据；被截断的只是最终集合中的隶属。索引之所以换成键 # (toℕ i) 而非直接使用，是因为公式语言必须能够谈论键，而公式所谈论的是集合，在这里就是数码。
env : ∀ {n} → (Fin n → V ℓ) → V ℓ env {n} g = sett (Lift {ℓ-zero} {ℓ} (Fin n)) (λ li → pr (# (toℕ (lower li))) (g (lower li)))
这个图是函数性的：一个对属于 env g 在键 i 处，恰当其第二分量为值 g i。这是关于隶属的外延陈述，也正是这个编码不只可定义、而且可用于查值的原因。
论证沿着键的三个层次展开。作证的条目是一个 Kuratowski 对，而对是单射的，故其键等于所问的键。键是数码，数码是单射的，故底层的序号作为自然数相等。最后 Fin n 嵌入自然数，故两个序号是同一个索引，值分量便说明那里放着 g i。反向只需展示 i 处的条目本身。
陈述是命题的等式：键 i 处的对属于图，这一命题恰为 v ≡ g i，并附有其命题性的证明，它来自 V ℓ 是 h-集合这一事实。命题之间的等价可转换为真值之间的路径，故引理由两个方向各一的蕴含拼成。
lookup-spec : ∀ {n} (g : Fin n → V ℓ) (i : Fin n) (v : V ℓ) → (pr (# (toℕ i)) v ∈ env g) ≡ ((v ≡ g i) , setIsSet v (g i)) lookup-spec {n} g i v = ⇔toPath fwd bwd where step : (lj : Lift {ℓ-zero} {ℓ} (Fin n))
正向作用于被截断的见证，故情形分析被分解为显式条目上的一个普通函数。其输入是一条路径，断言图中某个条目等于所问的对；其输出即目标 v ≡ g i。由于目标是命题，把截断消入其中是合法的；没有任何条目被提取为普通数据。
→ pr (# (toℕ (lower lj))) (g (lower lj)) ≡ pr (# (toℕ i)) v → v ≡ g i step lj e = sym (ps .snd) ∙ cong g (inj-toℕ (#-inj′ (ps .fst))) where ps : (# (toℕ (lower lj)) ≡ # (toℕ i)) × (g (lower lj) ≡ v)
对的单射性把假设的等式拆成键的路径与值的路径。值路径取反向即目标的一半。键路径说两个数码相符；数码的单射性连同到自然数的嵌入把它化为序号本身的相等，再用 g 作用得到另一半。反向直接展示 i 处的条目：截断见证是提升后的索引，路径由对构造子作用于反向假设填充。这里没有挑选任何典范见证，也不主张见证唯一。
ps = pr-inj e fwd : ⟨ pr (# (toℕ i)) v ∈ env g ⟩ → v ≡ g i fwd = PT.rec (setIsSet v (g i)) (λ { (lj , e) → step lj e }) bwd : v ≡ g i → ⟨ pr (# (toℕ i)) v ∈ env g ⟩ bwd e = ∣ lift i , cong (pr (# (toℕ i))) (sym e) ∣₁
识别后继索引
有界公式 sucAt i j 表示 j 处的值是 i 处的值的 von Neumann 后继；sucAt-adequate 证明该公式在环境下的满足恰好就是这两个值的相等。
环境的扩张把每个序号上移一位，而在数码上这一移位就是 von Neumann 后继。因此要下降到约束之下的证书机制，必须能说出「这个序号是那个的后继」。语言中没有后继符号，故该关系只用隶属来说，分三条子句：小者属于大者；属于小者的一切都属大者；而属于大者的一切仅仅属于小者或与之相等。
三条有界子句即可做到：小者属于大者；小者中的隶属可转移到大者中；而大者中的隶属只被仅仅分类，为属于小者或等于小者。有界量词约束 var zero，量词体内的其余变元按移位后的槽位读取，故体内的 var (suc i) 指的正是下降前 var i 的值。第二、三条子句恰说明：大者除小者的成员与小者自身之外别无成员，这正是「是其后继」的外延内容。有界性由 Δ₀-sucAt 单独记录：合取、有界全称量词，以及叶子的隶属与相等，都保持 Δ₀。
sucAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n sucAt i j = (var i ∈̇ var j) ∧̇ ((∀̇∈ (var i) (var zero ∈̇ var (suc j))) ∧̇ (∀̇∈ (var j) ((var zero ∈̇ var (suc i)) ∨̇ (var zero ≐ var (suc i))))) Δ₀-sucAt : ∀ {n} (i j : Fin n) → Δ₀ (sucAt i j)
充分性证明建立在集合层面的宿主级刻画之上。它说：把三条公式子句读作关于集合 I 与 J 的事实，它们成立恰当 J 与 sucV I 作为集合相等时。
Δ₀-sucAt i j = δ-∧ δ-∈ (δ-∧ (δ-∀∈ δ-∈) (δ-∀∈ (δ-∨ δ-∈ δ-≐))) private suc-char : (I J : V ℓ) → ⟨ I ∈ J ⟩ → ((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩)
正向引理把三条子句作为假设，落在集合层面：I 属于 J；I 中的隶属可转移到 J 中；J 的每个成员仅仅属于 I 或等于 I。结论是路径 J ≡ sucV I，即集合的真正相等，而非隶属间的双条件。
→ ((z : V ℓ) → ⟨ z ∈ J ⟩ → ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁) → J ≡ sucV I suc-char I J hIJ mono cover = extensionality J (sucV I) (sub₁ , sub₂) where sub₁ : ⟨ J ⊆ sucV I ⟩
相等由外延性产生，拆成两个包含。第一个包含把 J 的每个成员送过去：分类假设给出一个截断的析取，两个析取支都被消入「属于 sucV I」这一取值为命题的目标。左支的成员经后继的并集分支转移；右支的成员就是 I 本身，它作为自身的顶端元素属于 sucV I。
sub₁ z z∈ₛJ = PT.rec ((z ∈ₛ sucV I) .snd) (Sum.rec (λ h → ∈∈ₛ {a = z} {b = sucV I} .fst (∈sucV-inl {A = I} {x = z} h)) (λ e → subst (λ w → ⟨ w ∈ₛ sucV I ⟩) (sym e) (∈∈ₛ {a = I} {b = sucV I} .fst (self∈sucV I))))
第二个包含把 sucV I 的成员读回 J。属于后继这一事实由带两个分支的消去器分类，分类假设的截断正是在此处被消费：消去器的目标是命题 z ∈ J，故对截断分类作情形分析是合法的。两个分支各自使用已有的子句：把成员从 I 中转移过来，或把它改写成 I。
(cover z (∈∈ₛ {a = z} {b = J} .snd z∈ₛJ)) sub₂ : ⟨ sucV I ⊆ J ⟩ sub₂ z z∈ₛs = ∈∈ₛ {a = z} {b = J} .fst (∈sucV-elim {A = I} {x = z} {P = ⟨ z ∈ J ⟩} ((z ∈ J) .snd) (∈∈ₛ {a = z} {b = sucV I} .snd z∈ₛs)
逆命题 suc-intro 把刻画沿反方向运行。给定 J ≡ sucV I，前两条子句由后继集合的隶属事实搬运到 J 得到。第三条先把 J 的成员搬到 sucV I，再用后继隶属的消去器，直接得到所需的截断分类。因此这一方向并不消除一条作为假设给出的截断分类。
(λ h → mono z h) (λ e → subst (λ w → ⟨ w ∈ J ⟩) (sym e) hIJ)) suc-intro : (I J : V ℓ) → J ≡ sucV I → ⟨ I ∈ J ⟩ × (((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩)
每条子句都是把关于 sucV I 的隶属事实沿已给路径搬运得到，方向以使事实落在 J 上为准。第一条搬运「I 属于自己的后继」这一事实；第二条逐成员搬运转移规则 ∈sucV-inl。
× ((z : V ℓ) → ⟨ z ∈ J ⟩ → ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁)) suc-intro I J e = subst (λ w → ⟨ I ∈ w ⟩) (sym e) (self∈sucV I) , (λ z h → subst (λ w → ⟨ z ∈ w ⟩) (sym e) (∈sucV-inl {A = I} {x = z} h)) , (λ z z∈J → ∈sucV-elim {A = I} {x = z} {P = ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁} squash₁
第三条子句是对 J 成员的分类，其目标正是那个截断析取本身。后继消去器以该截断为消除目标而施用，于是它的两个分支情形各由重新截断相应分支来回应。三条子句齐备后，充分性陈述取得与 lookup-spec 相同的形状：γ 满足 sucAt i j 这一命题，就是「j 处的值等于 i 处的值的 von Neumann 后继」。
(subst (λ w → ⟨ z ∈ w ⟩) e z∈J) (λ h → ∣ inl h ∣₁) (λ q → ∣ inr q ∣₁)) sucAt-adequate : ∀ {n} (i j : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ sucAt i j) ≡ ((⟦ var j ⟧ γ ≡ sucV (⟦ var i ⟧ γ)) , setIsSet _ _)
两条引理与充分性陈述恰好吻合。正向：合取的满足拆成三条子句，suc-char 把它们当作三条假设，转为语义等式；由于结论是命题，量词数据的截断结构得以合法通过消除。反向：suc-intro 从语义等式产出三条子句。两个方向复合成一条真值路径，这正是充分性引理的形态。
sucAt-adequate i j γ = ⇔toPath (λ { (h₁ , h₂ , h₃) → suc-char (⟦ var i ⟧ γ) (⟦ var j ⟧ γ) h₁ h₂ h₃ }) (suc-intro (⟦ var i ⟧ γ) (⟦ var j ⟧ γ))
移位一个条目
shiftPairAt p' p 识别如下情形：把 p 处有序对的数码键换成其 von Neumann 后继、值保持不变，便得到 p' 处的有序对。
扩张环境不只是在零键处插入一个新条目，它还给旧条目重新编号：原来键为 # i 的条目变为键为 # (suc i)。本节把这一重编号的单步分离出来，给它一个有界的描述。由于一个有界量词只能约束集合的一个成员，而一个 Kuratowski 对的条目一次只给出索引与值之一，公式便依次运行五层有界量词，同时持有两个条目、各自的索引以及共享的值。其主体随后是配对读式一章的两条 Kuratowski 读式，加上上一节的后继读式，合起来恰好说明：两个条目共享一个值，而两个键相差一个后继步。
公式是对 p 处之值的五层有界量化。每个有界存在量词都给环境增添一个槽位，故被约束的见证按已进入量词的层数落在确定的位置上：前三层量词产出 p 处的条目、其索引与值。
shiftPairAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n shiftPairAt p' p = ∃̇∈ (var p) (∃̇∈ (var zero) (∃̇∈ (var (suc zero))
剩下的两层量词产出 p' 处的条目及其索引。至此主体可以同时使用全部五件东西：原条目、其索引、其值、移位条目、以及移位索引。
(∃̇∈ (var (suc (suc (suc p')))) (∃̇∈ (var zero) ( prAt (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) ∧̇ ( prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero))
主体是对这五个见证的三条有界断言的合取。两条 Kuratowski 读式说：原条目是其索引与值的对，移位条目是移位索引与同一个值的对；后继读式说：移位索引是原索引的 von Neumann 后继。合起来读，移位条目在升高一个后继步的键处携带同一个值。
∧̇ sucAt (suc (suc (suc zero))) zero )))))) shiftPairAt-adequate : ∀ {n} (p' p : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ shiftPairAt p' p) ≡ (∥ Σ[ i ∈ V ℓ ] Σ[ v ∈ V ℓ ] ((⟦ var p ⟧ γ ≡ pr i v) × (⟦ var p' ⟧ γ ≡ pr (sucV i) v)) ∥₁ , squash₁)
充分性陈述记录了这种嵌套量化的满足实际提供的东西：一个仅仅存在的断言。它说槽位 p 处的集合仅仅是某个索引与值的对，槽位 p' 处的集合仅仅是该索引的后继与同一个值的对。截断忠实于公式本身：公式中没有挑出任何一个条目的特定分解，也不需要。
shiftPairAt-adequate p' p γ = ⇔toPath fwd bwd where P = ⟦ var p ⟧ γ P' = ⟦ var p' ⟧ γ Tgt : Type (ℓ-suc ℓ)
正向要把一串截断的见证转换成截断目标的一个居民，其做法是在五个见证全部显式之后一次性使用它们。此时可用的假设是主体的三个合取支，各自在扩张了全部五个被约束见证的环境中陈述；结论是截断存在陈述的一个居民。
Tgt = ∥ Σ[ i ∈ V ℓ ] Σ[ v ∈ V ℓ ] ((P ≡ pr i v) × (P' ≡ pr (sucV i) v)) ∥₁ conclude : (c i v c' j : V ℓ) → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ) ⊨ prAt (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) ⟩ → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)
五个见证都显式之后，以索引 i、值 v 与两条路径等式即可填入截断目标。三条满足假设经前面证明的充分性引理给出这些等式，再沿所得路径搬运，使端点与目标对齐。外层目标的命题性用于周围的截断消除；路径搬运本身并不要求这一条件。
⊨ prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) ⟩ → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ) ⊨ sucAt (suc (suc (suc zero))) zero ⟩ → Tgt conclude c i v c' j sat₁ sat₂ sat₃ = ∣ i , v
配对读式的充分性引理重新解释槽位 p 处的满足假设：它恰断言该处的条目是约束索引与约束值的 Kuratowski 对。这把第一条满足证明转成了所记录的两条等式中的第一条：P ≡ pr i v。
, subst ⟨_⟩ (prAt-adequate (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₁ , (subst ⟨_⟩
第二条配对读式的假设给出等式 P' ≡ pr j v，后继读式的假设给出 j ≡ sucV i。把第二条复合进第一条，并让后继运算作用于对的第一个分量，便产生所记录的第二条等式：P' ≡ pr (sucV i) v。它与第一条等式合起来恰是目标：两个条目共享一个值，且第二个键是第一个键的 von Neumann 后继。
(prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₂ ∙ cong (λ z → pr z v) (subst ⟨_⟩
拼装好的索引、值与两条等式随后被截断入目标。至此充分性的正向完成，它逐层剥开五个量词。每层都是截断的存在，故每次消除都必须落入命题；目标恰被截断，正是为了使这层消除嵌套合法。
(sucAt-adequate (suc (suc (suc zero))) zero (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₃)) ∣₁ fwd : ⟨ γ ⊨ shiftPairAt p' p ⟩ → Tgt fwd = PT.rec squash₁ (λ { (c , _ , h₁) → PT.rec squash₁
最内层的消除到达三条满足证明，正向证明随之完成。注意这五个见证从未成为消除之外的普通数据：每次消除都把一个截断层消耗进一个命题，见证只存在于这条链之内。
(λ { (i , _ , h₂) → PT.rec squash₁ (λ { (v , _ , h₃) → PT.rec squash₁ (λ { (c' , _ , h₄) → PT.rec squash₁ (λ { (j , _ , sat₁ , sat₂ , sat₃) → conclude c i v c' j sat₁ sat₂ sat₃ }) h₄ })
反向依靠引入而非分析。给定一个索引、一个值，以及把两个槽位与相应配对等同的两条等式，需要产出一条满足证明；它所需的每件东西都是普通的集合构造：条目集合用配对运算造出，其隶属由分量引入规则给出。
h₃ }) h₂ }) h₁ }) build : (i v : V ℓ) → P ≡ pr i v → P' ≡ pr (sucV i) v → ⟨ γ ⊨ shiftPairAt p' p ⟩ build i v eP eP' =
最外层存在的第一个见证就是对 ⁅ i , v ⁆ 本身。它属于槽位 p 处的集合，因为假定的等式把该集合等同于 pr i v，而由分量引入规则，无序对 ⁅ i , v ⁆ 就在其自身的 Kuratowski 编码之内；沿等式搬运即把隶属移到正确的位置。随后打开这个对无需任何工作：索引见证是 i，值见证是 v，各由一条分量规则给出。
∣ ⁅ i , v ⁆ , subst (λ z → ⟨ ⁅ i , v ⁆ ∈ z ⟩) (sym eP) (∈pair-introR {u = ⁅ i ⁆s} {v = ⁅ i , v ⁆} {y = ⁅ i , v ⁆} refl) , ∣ i , ∈pair-introL {u = i} {v = v} {y = i} refl , ∣ v , ∈pair-introR {u = i} {v = v} {y = v} refl
移位条目由 sucV i 与 v 经同一构造得到，移位索引见证就是后继集合本身。其余子句由两条假定的等式满足，充分性引理会把它们读回满足证明。正向不得不分析一个假想的见证，反向则只是装配公式要求的五个见证，截断的外层由一个显式见证填充。
, ∣ ⁅ sucV i , v ⁆ , subst (λ z → ⟨ ⁅ sucV i , v ⁆ ∈ z ⟩) (sym eP') (∈pair-introR {u = ⁅ sucV i ⁆s} {v = ⁅ sucV i , v ⁆} {y = ⁅ sucV i , v ⁆} refl) , ∣ sucV i
最内层的见证是移位后的条目 ⁅ sucV i , v ⁆，其索引见证就是后继集合 sucV i 本身，由 Kuratowski 对的左分量规则引入。剩下的是关于两个条目的子句。第一条由假定的等式 eP : ⟦ var p ⟧ γ ≡ pr i v 填入。该子句在扩张五次的环境中求值，槽位零至四依次放着 sucV i、移位后的对、v、i 与原对；被约束的变元占据这些槽位，故槽位 p 在其中读出的仍是 ⟦ var p ⟧ γ，恰为 eP 的左侧。配对读式的充分性引理把该子句的满足等同于这条等式，因此沿对称的充分性路径搬运 eP 即填入第一条子句。
, ∈pair-introL {u = sucV i} {v = v} {y = sucV i} refl , subst ⟨_⟩ (sym (prAt-adequate (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ)))
关于条目的第二条子句同样由 eP' 填入。槽位 p' 处的配对读式从槽位零取索引，而槽位零现在放着 sucV i；从槽位二取值，槽位二放着 v。于是充分性引理所期待的等式恰为 ⟦ var p' ⟧ γ ≡ pr (sucV i) v，即第二条假定。注意此处无需拆开移位后的条目本身：两条配对读式给出两个分解，而后继读式由于槽位零放着槽位三的后继而由 refl 填入，它记录了新键是旧键的后继且值保持不变。
eP , subst ⟨_⟩ (sym (prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ))) eP'
主体的最后一个合取支是上一节的后继读式，作用于两个索引见证。在拼装好的环境中，槽位三处的值是索引 i，槽位零处的值是它的 von Neumann 后继 sucV i，故该读式的刻画由自反路径 sucV i ≡ sucV i 见证，再经其充分性引理搬运为满足子句。至此主体的三条断言全部成立：两个条目都是真正的对且共享一个值，第二个键是第一个键的后继。这正是一条重编号条目的数学内容。
, subst ⟨_⟩ (sym (sucAt-adequate (suc (suc (suc zero))) zero (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ))) refl ∣₁
剩下的只是跨越五层嵌套有界存在量词的整理。每一层都是命题，因此逐层给出一个见证、并把它封为「仅仅在场」是合法的：并未在候选之间作选择，因为本无候选在竞争。每层存在量词各有见证之后，整条公式的满足证明便拼装完成。
∣₁ ∣₁ ∣₁ ∣₁
反向方向完成充分性定理。其输入是「存在索引与值以及两条等式」的截断存在，其输出是满足证明，而满足证明本身是命题。把截断消除到取值为命题的目标正是规则所允许的，因此假定的一对分解可在消除内部使用，尽管它不会在消除之外作为普通数据被取回。构造出的见证随后逐子句匹配公式，完成了这层等同：移位公式的满足作为真值，恰是「两个条目是以对的形式共享一个值且键相差一个后继」这一截断陈述。
bwd : Tgt → ⟨ γ ⊨ shiftPairAt p' p ⟩ bwd = PT.rec ((γ ⊨ shiftPairAt p' p) .snd) (λ { (i , v , eP , eP') → build i v eP eP' })
编码空条目
扩张后的环境的第零个新条目是带标签 # 0 的 Kuratowski 对，而 # 0 按定义就是空集。本节构造的读式识别这样的对，但只通过标签的数学性质提到它：一个成员是空的，这可用进入否定式公式的有界量化表达，无需任何常元。三条公式 sgl0At、pair0At 与 tag0At 分别说：一个集合是空集的单点集，是空集与给定集合的无序对，以及是由前两者装配的带标签对。
元层工作把这些公式的满足读式，即以谓词 Empty' (说一个集合没有成员) 表述的版本，转换为配对读式一章中 prChar-fwd 与 prChar-bwd 已接受的形状，在那里空集是直接点名的。由于没有成员的集合按外延性等于 ∅，两种表述描述的是同一数学内容；充分性引理 tag0At-adequate 把标签读式的满足等同于「带标签的集合等于 pr ∅ 作用于第二槽位之值」这条等式。
第一条读式在不点名空集的情况下描述单点集 {∅}。sgl0At k 对 k 处的值合取两条有界子句：仅仅有一个成员满足主体 ∀̇∈ (var zero) ⊥̇，且每个成员都满足。在有界量词之下，主体 ⊥̇ 恰在被量化的成员自身没有成员时成立，故每条子句都说其主语是空的。存在子句保证该值确实非空；没有它，空集自身也会满足该条件。两条子句合起来说：k 处的值有成员，且其成员全为空集，这在外延上把它确定为 {∅}。
sgl0At : ∀ {n} → Fin n → Formula (V ℓ) n sgl0At k = (∃̇∈ (var k) (∀̇∈ (var zero) ⊥̇)) ∧̇ (∀̇∈ (var k) (∀̇∈ (var zero) ⊥̇)) pair0At : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n pair0At k j = (∃̇∈ (var k) (∀̇∈ (var zero) ⊥̇))
第二条读式 pair0At k j 描述无序对 {∅, W}，其中 W 是原赋值槽位 j 处的值；进入新绑定后由 suc j 指向同一取值。它的三条子句是：k 处的值仅仅有一个空成员；j 处的值属于它；它的每个成员仅仅是空的或等于 W。第一子句正是单点集读式用过的那个空成员存在，第三子句是把第一分量固定为 ∅ 的配对分类。第三条公式 tag0At s x 把两条读式合并：s 处的值仅仅有一个成员满足空单点集子句，仅仅有一个成员满足空对子句，且每个成员仅仅满足其一。
∧̇ ((var j ∈̇ var k) ∧̇ (∀̇∈ (var k) ((∀̇∈ (var zero) ⊥̇) ∨̇ (var zero ≐ var (suc j))))) tag0At : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n tag0At s x = (∃̇∈ (var s) (sgl0At zero)) ∧̇ ((∃̇∈ (var s) (pair0At zero (suc x)))
在元层一侧，空性由私有谓词 Empty' z 表达：它是一个函数，取 z 的任意成员 y，返回空类型 ⊥* 的一个元素。这个函数表达 z 没有成员：任何声称的隶属都会产生空类型 ⊥* 的元素。它不同于对象语言中的否定式公式 ⊥̇，后者是语法。第一条引理 empty'→∅ 是通向被点名的空集的桥梁：凡使 Empty' 成立的集合都等于 ∅。
∧̇ (∀̇∈ (var s) (sgl0At zero ∨̇ pair0At zero (suc x)))) private Empty' : V ℓ → Type (ℓ-suc ℓ) Empty' z = (y : V ℓ) → ⟨ y ∈ z ⟩ → E.⊥* {ℓ-suc ℓ} empty'→∅ : (z : V ℓ) → Empty' z → z ≡ ∅
这座桥的证明是外延性，且两个方向都是空洞的。为证每个 y 属于 z 恰当其属于 ∅：设 y 属于 z，把 Empty' z 施于该隶属便得空类型的一个元素，由此可得任何结论，特别是属于 ∅。另一方向上，∅-empty 反驳任何属于 ∅ 的隶属，而由这个反驳同样可得属于 z。反向的桥 ∅→empty' 只需定义性路径：把 z 的一个隶属沿 e : z ≡ ∅ 搬运落入 ∅，在那里 ∅-empty 再次给出矛盾。于是 Empty' z 与 z ≡ ∅ 可以互换。
empty'→∅ z hz = extensionalV (λ y → ⇔toPath (λ h → E.rec (lower (hz y h))) (λ h → E.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst h)))) ∅→empty' : (z : V ℓ) → z ≡ ∅ → Empty' z ∅→empty' z e y y∈z = lift (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst (subst (λ w → ⟨ y ∈ w ⟩) e y∈z)))
两条读式的满足展开后，呈两个元层包裹的形状。EmptySgl w 由「w 有一个空成员」的截断存在，加上非截断的全称子句「每个成员都是空的」组成。EmptyPair W w 保留截断的空成员存在，把其余换成 W 属于 w，加上截断的分类：每个成员仅仅是空的或等于 W。截断的位置恰是公式的有界存在量词与截断析取所放置之处；特别地，任何时候都不会取出一个被选定的对分解。
EmptySgl : V ℓ → Type (ℓ-suc ℓ) EmptySgl w = ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → Empty' z) EmptyPair : V ℓ → V ℓ → Type (ℓ-suc ℓ) EmptyPair W w = ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁
对应的包裹直接点名空集。SglOf∅ w 断言 ∅ 属于 w 且 w 的每个成员都等于 ∅，因见证已给出而无需截断。PairOf∅ W w 断言 ∅ 与 W 属于 w 且每个成员仅仅是 ∅ 或 W；分类保持截断，与层级的无序对隶属一致，从那里并不能选出在哪一侧。这些恰是配对读式一章的配对刻画所消耗的形状，只是第一分量取在 ∅，于是剩下的全部任务就是在同一隶属事实的两种表述之间往返。
× (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ Empty' z ⊎ (z ≡ W) ∥₁)) SglOf∅ : V ℓ → Type (ℓ-suc ℓ) SglOf∅ w = ⟨ ∅ ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ ∅) PairOf∅ : V ℓ → V ℓ → Type (ℓ-suc ℓ) PairOf∅ W w = ⟨ ∅ ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ ∅) ⊎ (z ≡ W) ∥₁))
正向转换把「存在一个空成员」的截断陈述变成直接的事实：∅ 属于 w。层级中集合的隶属是一个命题，故把截断消除到 ⟨ ∅ ∈ w ⟩ 是合法的。在内部，显式给出的见证 z 带有隶属证明与 Empty' z 的证明，先由前一条引理把它与 ∅ 等同，其隶属便沿该路径搬运成 ∅ 的隶属。EmptySgl w 的其余部分随之整体转换：非截断的全称子句对 w 的每个成员 z 给出 Empty' z，同一引理再把它改写为 z ≡ ∅。
empty-member : (w : V ℓ) → ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ → ⟨ ∅ ∈ w ⟩ empty-member w = PT.rec ((∅ ∈ w) .snd) (λ { (z , hz , ez) → subst (λ u → ⟨ u ∈ w ⟩) (empty'→∅ z ez) hz }) EmptySgl→SglOf∅ : (w : V ℓ) → EmptySgl w → SglOf∅ w EmptySgl→SglOf∅ w (h₁ , hall) = empty-member w h₁ , (λ z hz → empty'→∅ z (hall z hz))
有序对情形沿用同一方案。EmptyPair→PairOf∅ 对第一分量复用空成员转换，W 的隶属保持不变，并逐成员改写分类：把「每个成员是空的或等于 W」的截断陈述，映射为把 Empty' 换成「等于 ∅」后的对应截断陈述。结果恰是以 ∅ 为基准的分类，且截断全程保留，并未被解析为选定的某一边。
EmptyPair→PairOf∅ : (W w : V ℓ) → EmptyPair W w → PairOf∅ W w EmptyPair→PairOf∅ W w (h₁ , hW , hall) = empty-member w h₁ , hW , (λ z hz → PT.map (Sum.map (empty'→∅ z) (λ e → e)) (hall z hz)) SglOf∅→EmptySgl : (w : V ℓ) → SglOf∅ w → EmptySgl w SglOf∅→EmptySgl w (h∅ , hall) =
反方向完全不需要寻找见证，因为空集从一开始就被点名。SglOf∅→EmptySgl 直接产出截断见证：∅ 按假定属于 w，而由沿定义性路径 ∅ ≡ ∅ 应用反向引理知它是空的。全称子句由同一引理朝另一方向转换。PairOf∅→EmptyPair 保留该见证，原样继承 W 的隶属，并逐点改写分类子句。
(∣ ∅ , (h∅ , ∅→empty' ∅ refl) ∣₁) , (λ z z∈w → ∅→empty' z (hall z z∈w)) PairOf∅→EmptyPair : (W w : V ℓ) → PairOf∅ W w → EmptyPair W w PairOf∅→EmptyPair W w (h∅ , hW , hall) = (∣ ∅ , (h∅ , ∅→empty' ∅ refl) ∣₁)
在这条有序对转换中，分类沿反方向运行：仅已知为 ∅ 或 W 的成员变成「空的或等于 W」的成员，第一分支用 ∅→empty'，第二分支无需改动。本节随后抽象出两个方向共享的模式。PairWitness P R Q 打包了从集合 Q 读出 Kuratowski 对刻画所需的三条子句：Q 的某个携带 P 的成员的截断存在，对 R 同样，以及给 Q 的每个成员指派 P 或 R 之一的截断二分。
, (hW , λ z z∈w → PT.map (Sum.rec (λ e → inl (∅→empty' z e)) (λ e → inr e)) (hall z z∈w)) PairWitness : (V ℓ → Type (ℓ-suc ℓ)) → (V ℓ → Type (ℓ-suc ℓ)) → V ℓ → Type (ℓ-suc ℓ) PairWitness P R Q = ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × P w) ∥₁ × (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × R w) ∥₁
上述的一切只是同一次转换应用三遍。map-witness 取一个 PairWitness P R Q 以及两条逐点蕴含，一条把每个 P w 送到 P' w，另一条把每个 R w 送到 R' w，并返回 PairWitness P' R' Q。这正是整节的形状：以空性为基准的谓词与以 ∅ 为基准的谓词，是关于同一集合的同一三子句结构的两种包装，而四条转换引理恰在两个方向提供所需的逐点蕴含。
× ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ P y ⊎ R y ∥₁)) map-witness : {P R P' R' : V ℓ → Type (ℓ-suc ℓ)} (Q : V ℓ) → ((w : V ℓ) → P w → P' w) → ((w : V ℓ) → R w → R' w) → PairWitness P R Q → PairWitness P' R' Q map-witness Q f g (h₁ , h₂ , h₃) =
于是正向定理 prChar∅-fwd 取三条以空性为基准的假设，其截断形状正是 tag0At 的满足呈现出来的形状，并得出路径 Q ≡ pr ∅ W。转换引理被应用一次，把假设变成关于 ∅ 的三子句；随后一般配对刻画由外延性把 Q 等同为 ∅ 与 W 的 Kuratowski 对。截断的见证从不被提取为普通数据；它们只在转换内部使用，而转换的输出正是该刻画所接受的取值为命题的子句。
PT.map (λ { (w , hw , h) → w , hw , f w h }) h₁ , PT.map (λ { (w , hw , h) → w , hw , g w h }) h₂ , (λ y hy → PT.map (Sum.map (f y) (g y)) (h₃ y hy)) prChar∅-fwd : (Q W : V ℓ) → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptySgl w) ∥₁
反向定理 prChar∅-bwd 与之互为镜像：从路径 Q ≡ pr ∅ W 出发，先把一般配对刻画反向运行，第一分量取 ∅、第二分量取 W，再把所得的每条子句转换成以空性为基准的对应物，返回三条这样的子句。两条定理就位后，tag0At s x 的满足即可与「槽位 s 处的值等于带标签对 pr ∅ (⟦ var x ⟧ γ)」互换，这正是下一节扩张子句要使用的读式。
→ ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptyPair W w) ∥₁ → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ EmptySgl y ⊎ EmptyPair W y ∥₁) → Q ≡ pr ∅ W prChar∅-fwd Q W h₁ h₂ h₃ = prChar-fwd Q ∅ W (fst h) (fst (snd h)) (snd (snd h)) where
中间谓词 PairWitness 使论证不依赖于 Q 的具体构造。改变的只有两个可能分量的逐点含义：先把空性换成「等于 ∅」，或沿反方向换回；随后即可应用一般的配对刻画，而无需重新打开截断见证。
h : PairWitness SglOf∅ (PairOf∅ W) Q h = map-witness Q EmptySgl→SglOf∅ (EmptyPair→PairOf∅ W) (h₁ , h₂ , h₃) prChar∅-bwd : (Q W : V ℓ) → Q ≡ pr ∅ W → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptySgl w) ∥₁ × (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptyPair W w) ∥₁
充分性引理与前面各读式一样，被陈述为真值之间的一条路径。左侧是 tag0At s x 的满足关系；右侧是命题「槽位 s 处的值等于 pr ∅ (⟦ var x ⟧ γ)」，即标签为空集、第二分量为槽位 x 处之值的 Kuratowski 对，并附上该相等类型为命题的证明，因为 V ℓ 是 h-集合。这恰好说明：编码后的第零个条目就是空标签与新值组成的对。
× ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ EmptySgl y ⊎ EmptyPair W y ∥₁)) prChar∅-bwd Q W e = map-witness Q SglOf∅→EmptySgl (PairOf∅→EmptyPair W) (prChar-bwd Q ∅ W e) tag0At-adequate : ∀ {n} (s x : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ tag0At s x) ≡ ((⟦ var s ⟧ γ ≡ pr ∅ (⟦ var x ⟧ γ)) , setIsSet _ _) tag0At-adequate s x γ = ⇔toPath
证明在两个方向各复合本节的两条引理。展开合取与三个有界量词的满足关系后，左边恰变成空单点集成员的截断存在、空对成员的截断存在与截断分类，这正是 prChar∅-fwd 所消耗的内容。反向则把路径 e 交给 prChar∅-bwd，其输出由语义重新组装为满足关系。两个方向都不检查任何集合是如何构造的；空性完全通过 Empty' 与「等于 ∅」之间的等价来处理。
(λ { (h₁ , h₂ , h₃) → prChar∅-fwd _ _ h₁ h₂ h₃ }) (λ e → prChar∅-bwd _ _ e)
扩张环境
向赋值前置一个值同时做两件事：新值落在索引零处，而每个旧序号上移一位。本节证明一条有界公式 consAt 恰好在编码图上表达这一变换，并且其充分性针对编码后的环境成立。
公式有三条子句：新集合的一个条目带有空标签与新值；旧图的每个条目都出现在新图中并已移位；新图的每个条目要么是那条新条目，要么是某个旧条目的移位。充分性陈述并不是说该公式仅以某种类似 cons 的方式把两个集合联系起来。在给定函数 g 与「旧槽位等于图 env g」这一假设后，它得出从新槽位到图 env (cons M g) 的路径。等式两侧都是层级中的集合，故证明是外延的：逐成员证明两个包含。一个方向用本章各读式对新集合的每个成员分类；另一方向按键逐个走遍 cons M g 的图。在索引处相符是定义性的，因为 suc k 的数码就是 k 的数码的后继。
宿主层运算 cons m g 是 Fin (suc n) 上的函数：索引零处返回 m，索引 suc i 处返回 g i。也就是前置一个值，而每个旧值只在序号上移一位之后仍取原值。公式 consAt e' m e 点名三个环境变元：e' 处的值是候选的扩张图，m 处的值是被前置的元素，e 处的值是被扩张的图。
cons : ∀ {ℓ'} {X : Type ℓ'} {n : ℕ} → X → (Fin n → X) → Fin (suc n) → X cons m g zero = m cons m g (suc i) = g i consAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n consAt e' m e =
consAt 的三条子句与 cons 的三个定义等式一一对应。在 γ 下读：e' 处的值仅仅有一个成员满足带标签对读式 tag0At zero (suc m)，即它持有一个标签为空、第二分量为 m 处之值的条目；e 处之值的每个条目仅仅在 e' 处之值中有一个移位，由 shiftPairAt 表述且旧条目放在靠后的槽位；而 e' 处之值的每个条目仅仅是那条带标签的零条目，或 e 处之值某条目的移位。每条子公式都由有界量词、等式与前面两条读式构成，故检查器把整个合取认证为 Δ₀，由 Δ₀-consAt 一次性记录。
(∃̇∈ (var e') (tag0At zero (suc m))) ∧̇ ((∀̇∈ (var e) (∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero)))) ∧̇ (∀̇∈ (var e') ((tag0At zero (suc m)) ∨̇ (∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero))))) Δ₀-consAt : ∀ {n} (e' m e : Fin n) → Δ₀ (consAt e' m e)
充分性引理带有一条额外假设，而正是它使命题为真。consAt 的满足本身只说新集合与旧集合处于 cons 关系；要把旧集合指认为一个图，引理额外给定长度为 k 的函数 g 与路径 ⟦ var e ⟧ γ ≡ env g。这正是证书所持的编码形式：候选环境以集合的形式出现在槽位中，而该假设把这个集合等同于它所编码的赋值的图。
Δ₀-consAt e' m e = checkΔ₀ (consAt e' m e) tt consAt-adequate : ∀ {n} (e' m e : Fin n) (γ : (V ℓ) ^ n) {k : ℕ} (g : Fin k → V ℓ) → ⟦ var e ⟧ γ ≡ env g → (γ ⊨ consAt e' m e)
结论是对新槽位的同类指认：e' 处的值等于 cons M g 的图，其中 M 是 m 处的值。与前面的读式一样，陈述是真值之间的一条路径，等式的命题性由 V ℓ 的 h-集合性质提供。缩写 M、E、E' 命名三个槽位处的值，⇔toPath 把论断归约为两个包含。
≡ ((⟦ var e' ⟧ γ ≡ env (cons (⟦ var m ⟧ γ) g)) , setIsSet _ _) consAt-adequate e' m e γ {k} g hE = ⇔toPath fwd bwd where M = ⟦ var m ⟧ γ E = ⟦ var e ⟧ γ
辅助引理 shift-path 一次性记录重编号算术：若两个编码条目作为对相等，则把两侧的键都换成各自的 von Neumann 后继、值保持不变后的条目也相等。Kuratowski 对的单射性 pr-inj 把假定路径拆成键的路径与值的路径，再用 cong₂ 在移位后的对构造子下重新组合。
E' = ⟦ var e' ⟧ γ G' : Fin (suc k) → V ℓ G' = cons M g shift-path : {a b x y : V ℓ} → pr a x ≡ pr b y → pr (sucV a) x ≡ pr (sucV b) y shift-path {a} {b} {x} {y} e = cong₂ (λ a b → pr (sucV a) b) (fst p) (snd p)
正向包含取公式的第三条子句，把它变成真正的隶属陈述。其假设说：E' 的每个成员 y，仅仅或者在扩张了 y 的环境中满足带标签零读式，或者满足一个有界存在式，其见证是 E 中移位到 y 的条目。目标是 y 属于 env G'，即扩张后赋值的图。注意假设的形状：它恰如公式的有界全称量词所产出的那个截断析取。
where p : (a ≡ b) × (x ≡ y) p = pr-inj e classify : ((y : V ℓ) → ⟨ y ∈ E' ⟩ → ∥ ⟨ (y ∷ γ) ⊨ tag0At zero (suc m) ⟩
截断析取只能消除到取值为命题的目标，而「属于 env G'」正是命题。随后两个分支分别处理：第一分支接收带标签零读式的满足，产出图的零键。
⊎ ⟨ (y ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁) → (y : V ℓ) → ⟨ y ∈ E' ⟩ → ⟨ y ∈ env G' ⟩ classify h₃ y y∈E' = PT.rec ((y ∈ env G') .snd) (Sum.rec (λ tsat →
第一分支中，成员 y 在 y ∷ γ 中满足 tag0At zero (suc m)，该读式的充分性引理把满足转换为路径 y ≡ pr ∅ M：槽位零处的值就是 y 本身，而新绑定之下的 suc m 仍指向原赋值槽位 m 的取值。反转这条路径得 pr ∅ M ≡ y，恰是 env G' 在键零处的条目，因为 G' zero 化归为 M，零的数码化归为空集。于是见证就是 lift zero 配上该路径。
∣ lift zero , sym (subst ⟨_⟩ (tag0At-adequate zero (suc m) (y ∷ γ)) tsat) ∣₁) (λ ssat → PT.rec ((y ∈ env G') .snd) (λ { (p , p∈E , sh) → PT.rec ((y ∈ env G') .snd) (λ { (li , peq) → PT.rec ((y ∈ env G') .snd)
第二分支是移位情形，它依次打开三层嵌套的截断。有界存在式的满足仅仅给出 E 的一个条目 p，以及关于二元环境 p ∷ y ∷ γ 的一条移位子句；shiftPairAt 的充分性引理把该子句转换为集合 i 与 v 的仅仅存在，使 p ≡ pr i v 且 y ≡ pr (sucV i) v。这里两个槽位的角色很关键：在 shiftPairAt (suc zero) zero 中，旧条目坐在靠后的槽位，被移位者坐在槽位零，故 y 是带后继键的那个对。
(λ { (i , v , epv , eyv) → ∣ lift (suc (lower li)) , sym (shift-path (sym epv ∙ sym peq)) ∙ sym eyv ∣₁ }) (subst ⟨_⟩ (shiftPairAt-adequate (suc zero) zero (p ∷ y ∷ γ)) sh) })
在移位情形中，一旦旧条目背后的索引 i 与值 v 显式可得，env G' 中的隶属便可由扩张后赋值的图直接拼出。图在后继键处的条目携带旧值，故所需的见证是索引 suc (lower li) 连同从该条目到 y 的一条路径。这条路径由三个等式复合：旧条目等于对 pr i v；把两侧的键都换成 von Neumann 后继后，它变成带后继键、值不变的对；而 env G' 在该键处的条目等于 y。这一复合记录的正是该情形的数学内容：新键是旧键的后继，且值保持不变。
(subst (λ z → ⟨ p ∈ z ⟩) hE p∈E) }) ssat)) (h₃ y y∈E') covered : ⟨ γ ⊨ ∃̇∈ (var e') (tag0At zero (suc m)) ⟩ → ((p : V ℓ) → ⟨ p ∈ E ⟩
移位情形还剩一步。条目 p 是作为 E 的成员找到的，而论证所需的图隶属在 env g 中，假设 E ≡ env g 把这条隶属沿路径搬运过去。在图内部，第一节证明的查值引理辨认出见证所指索引的键处存放的值。至此第一个包含完成：新集合的每个成员仅仅落入扩张后赋值的图。
→ ⟨ (p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero)) ⟩) → (y : V ℓ) → ⟨ y ∈ env G' ⟩ → ⟨ y ∈ E' ⟩ covered h₁ h₂ y y∈G' = PT.rec ((y ∈ E') .snd) (λ { (lj , eq) → byKey (lower lj) eq }) y∈G'
反向包含要证明：扩张后赋值的图的每个成员都属于新集合。图中的隶属是截断的纤维数据：一个图索引，加上说该索引处条目等于给定元素的路径。于是成员 y 连同它的索引与条目路径一起被读出，随后证明对索引分情形，因为 cons 的两条定义等式恰好产出两类条目：索引零处的新条目，以及各后继索引处的移位旧条目。
where byKey : (j : Fin (suc k)) → pr (# (toℕ j)) (G' j) ≡ y → ⟨ y ∈ E' ⟩ byKey zero eq = PT.rec ((y ∈ E') .snd) (λ { (q , q∈E' , tsat) → subst (λ z → ⟨ z ∈ E' ⟩)
零键情形中，条目等式按定义化归为「带空标签、值为 M 的条目等于 y」。公式的第一条子句仅仅给出新集合的一个成员 q，其带标签条目是空标签与 M 配成的对；它的充分性引理把满足关系变成恰好那条等式。把两条路径链接起来得 q ≡ y，沿它搬运 q 的隶属便得 y 在新集合中的隶属。除这条等式外并未使用 q 的任何信息，故第一条子句内部的截断见证只被消除进一个命题，恰如所需。后继情形则反向运行该论证：条目等式此时点名了 g 的一个旧条目，而公式的第二条子句必须在新集合中产出它的移位。
(subst ⟨_⟩ (tag0At-adequate zero (suc m) (q ∷ γ)) tsat ∙ eq) q∈E' }) h₁ byKey (suc i₀) eq = PT.rec ((y ∈ E') .snd) (λ { (p' , p'∈E' , sh) → PT.rec ((y ∈ E') .snd)
后继情形中，公式的移位子句给出索引 i、值 v 以及两条等式：旧条目等于对 pr i v，候选者等于移位后的对 pr (sucV i) v。目标是得到从候选者到成员 y 的路径，而纤维等式提供后继键处的移位图条目，它等于 y。由于后继索引的数码是原数码的后继，把对 pr i v 的两个键都换成各自后继后，恰好落在那个图条目上。三条等式复合成所需的路径，沿它搬运候选者的隶属即闭合此情形。
(λ { (i , v , epv , ep'v) → subst (λ z → ⟨ z ∈ E' ⟩) (ep'v ∙ shift-path (sym epv) ∙ eq)
还差一个输入。移位子句是一条满足陈述，它所在环境的第二槽必须真的存放旧条目 pr (# (toℕ i₀)) (g i₀) 本身，而公式的第二条子句提供相应的隶属。查值引理正是在此处被使用：在 i₀ 的键处，g 的图恰好存放 g i₀，由索引与 refl 组成的典范纤维见证这条隶属。沿「旧集合等于 g 的图」这条假设搬运，便把它变成编码环境中的隶属。
p'∈E' }) (subst ⟨_⟩ (shiftPairAt-adequate zero (suc zero) (p' ∷ pr (# (toℕ i₀)) (g i₀) ∷ γ)) sh) }) (h₂ (pr (# (toℕ i₀)) (g i₀)) (subst (λ z → ⟨ pr (# (toℕ i₀)) (g i₀) ∈ z ⟩) (sym hE) ∣ lift i₀ , refl ∣₁))
两个包含都建立之后，充分性引理的正向只需一次引用累积层级的外延性：成员相同的两个集合相等。公式的三条子句对每个元素 y 给出隶属比较的两个方向：从新集合的成员到扩张后赋值的图，再从图回到新集合。沿这个方向读，公式的满足被转换成编码图之间的相等。引理剩下的方向则从这样的相等构造满足关系。
fwd : ⟨ γ ⊨ consAt e' m e ⟩ → E' ≡ env G' fwd (h₁ , h₂ , h₃) = extensionalV (λ y → ⇔toPath (classify h₃ y) (covered h₁ h₂ y)) bwd : E' ≡ env G' → ⟨ γ ⊨ consAt e' m e ⟩ bwd e'eq =
反向从把新集合与扩张后赋值的图等同起来的那条路径出发，直接构造三条满足子句。第一条给出键零处的条目：按 cons 的定义等式，图在索引零处的隶属成立，而假定的路径把它转移到新集合中的隶属。带标签条目的子句随后直接成立，因为带空标签、值为 M 的条目按构造就是对 pr ∅ M，而零的数码就是空集。
∣ pr (# 0) M , subst (λ z → ⟨ pr (# 0) M ∈ z ⟩) (sym e'eq) ∣ lift zero , refl ∣₁ , subst ⟨_⟩ (sym (tag0At-adequate zero (suc m) (pr (# 0) M ∷ γ))) refl ∣₁ , (λ p p∈E → PT.rec (((p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero))) .snd)
第二条子句要对旧环境的每个成员给出它在新集合中的移位对应物。该成员的隶属沿假设搬运到 g 的图中，在那里查值引理读出一个索引以及把条目与该成员等同的等式。移位后的条目于是是以后继数码为键、值不变的对；它在新集合中的隶属同样来自扩张后赋值的图，位于后继索引处，再经假定的路径转移。剩下的只是移位公式本身的满足证书。
(λ { (li , peq) → ∣ pr (# (suc (toℕ (lower li)))) (g (lower li)) , subst (λ z → ⟨ pr (# (suc (toℕ (lower li)))) (g (lower li)) ∈ z ⟩) (sym e'eq) ∣ lift (suc (lower li)) , refl ∣₁ , subst ⟨_⟩
该证书靠反向运行移位的充分性引理得到。引理对公式的解读要求一个索引、一个值和两条等式：一条把旧条目与查值所得索引处的对等同；另一条说移位后的对就是移位后的条目本身，这一点按计算成立。由于充分性陈述是命题之间的相等，沿它搬运 refl 便得所需的满足，公式的第二条子句对该成员宣告完成。
(sym (shiftPairAt-adequate zero (suc zero) (pr (# (suc (toℕ (lower li)))) (g (lower li)) ∷ p ∷ γ))) ∣ # (toℕ (lower li)) , g (lower li) , sym peq , refl ∣₁ ∣₁ }) (subst (λ z → ⟨ p ∈ z ⟩) hE p∈E)) , (λ p' p'∈E' → PT.rec squash₁
第三条子句是分类子句：新环境的每个成员都必须仅仅满足两条带标签子句之一。为使用它，先把 E' 的成员 p' 沿路径 e'eq 搬运为编码图 env G' 中的隶属，那是截断的纤维数据：一个索引 j，以及说该键处条目等于 p' 的等式 pr (# (toℕ j)) (G' j) ≡ p'。随后按索引分情形，因为 cons 后的图恰有两类条目，对应定义 cons 的两条等式。由于目标是一个由两个命题组成的截断析取，每个情形都可以在相应析取支下给出自己的子句，而截断把情形划分包裹起来。
(λ { (lj , eq) → byKey' p' (lower lj) eq }) (subst (λ z → ⟨ p' ∈ z ⟩) e'eq p'∈E')) where byKey' : (p' : V ℓ) (j : Fin (suc k)) → pr (# (toℕ j)) (G' j) ≡ p'
索引零处 G' 的条目是新条目：等式为 pr (# 0) M ≡ p'。在调整路径方向之后，这恰好是说 p' 带有以 M 为值的空标签。带标签读式的充分性引理把其满足命题等同于等式 ⟦ var zero ⟧ (p' ∷ γ) ≡ pr ∅ M，而 # 0 计算为 ∅。于是取反向的等式、沿充分性路径搬运，便得到左边的析取支。
→ ∥ ⟨ (p' ∷ γ) ⊨ tag0At zero (suc m) ⟩ ⊎ ⟨ (p' ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁ byKey' p' zero eq = ∣ inl (subst ⟨_⟩ (sym (tag0At-adequate zero (suc m) (p' ∷ γ))) (sym eq)) ∣₁ byKey' p' (suc i₀) eq =
后继索引处，G' 的条目是一个移位后的旧条目，右边的析取支必须用移位公式给出证书。移位公式要求的纤维有五个分量，其中「作为集合的索引」与值槽是直接的。旧条目槽需要 pr (# (toℕ i₀)) (g i₀) 属于旧环境，这由 lookup-spec 得到：在 env g 的索引 i₀ 处，该键的条目正是以 g i₀ 为值的对，再沿 hE 搬运即得 E 中的隶属。移位条目槽由以数码为键的条目 pr (# (toℕ i₀)) (g i₀) 本身填入，按 eq 它等于 p' (方向待调整)。
∣ inr ∣ pr (# (toℕ i₀)) (g i₀) , subst (λ z → ⟨ pr (# (toℕ i₀)) (g i₀) ∈ z ⟩) (sym hE) ∣ lift i₀ , refl ∣₁ , subst ⟨_⟩ (sym (shiftPairAt-adequate (suc zero) zero
剩下的两条路径补全纤维。旧条目路径是定义性的：所选的索引与值恰是 i₀ 的数码与 g i₀。移位路径取反向的 eq，因为移位条目须等于以后继键构成的那个对，而按假定它就是 p'。反向运行 shiftPairAt (suc zero) zero 的充分性引理，把装配好的纤维转换为它的满足关系，置于右边析取支之下。于是情形划分的两个分支都只是「仅仅」给出各自的子句，恰如第三条子句的截断析取所要求的那样。
(pr (# (toℕ i₀)) (g i₀) ∷ p' ∷ γ))) ∣ # (toℕ i₀) , g i₀ , refl , sym eq ∣₁ ∣₁ ∣₁
小结
本章把满足关系子句所需的两种环境操作化为关于集合的陈述：查出一个值，以及在量词之下扩张赋值。
编码本身是 env，它把赋值存成以数码为键的对的图，而 lookup-spec 证明该图是函数性的：一个对在键 i 处属于图，恰在其值为 g i 时成立。在运算一侧，sucAt 用语言所能表达的三条隶属子句刻画一个集合的 von Neumann 后继，shiftPairAt 识别单个重编号的条目。consAt 把这些装配成整个变换：在旧槽位等于 g 的图的假设下，公式的满足就是新槽位与 cons M g 的图的相等，其证明由两个包含经集合外延性比较而成，截断的见证只被消除进命题。