BedrockThe codes, as one set
至此每一章都小心地说过：全体码之集不是 L 的元素，而且没有东西需要它。现在有两样东西需要它了，而它们想要的不是同一个集合。可定义幂集以语法为索引类型，Def A = sett (Formula ⟪A⟫ 1) defSet，故在一个阶段处内化可定义性，就意味着从模型内部点名该阶段之上的一元公式，而公式只能点名集合。满足关系那场递归想要一个对诸子码封闭的索引集，而量词的子公式住在高一级的元数上，故它想要的是每个元数处的诸键。
两个集合都不是靠把诸码收集起来造出的。各自都是从一个超集中切出来的：smallDom 把 L 元素的任意小族装进单一阶段，而诸键正是这样一个族，且 L 内部的分离对任意复杂度的公式成立。故本章是两条只差一个合取项的对象语言谓词，以及各自适足性的两个方向。
那条谓词有两个合取项，而二者分量不等。第二项「仅仅存在一个等于 A 的载体、以及一个集合 C，x 是它的成员，C 封闭且 C 在该载体上成形」是若干无界存在，在此处不费分文：满足关系是在类模型处读的，存在量词在 L 上取值，无须任何阶段去反射任何东西。
第一个合取项才是承重的那个，而它就是本章的发现。recover 收下的不是「封闭且成形之集的一个成员」；它收下的是以某个已言明元数处的键的形式递交过来的成员，而 closedAt 与 shapedAt 都没有约束元数那一位。形状把元数存在量化，且对它不加任何条件，故一个持有「第一分量压根不是数码的对」的集合同样满足两半，而解码对那个对无话可说。这笔债在欠下之处已被记下，而此处正是偿付之处：那条谓词从外面说出，x 是一个第一分量为数码的对。是哪个数码，正是两条谓词之间唯一的差别。一元那个集合把它点名，全元数那个集合把它绑定、只要求它属于 ωʟ，而本章其余一切逐字共享。
载体是一位，而把那一位变成常元的，是它上面那一层绑定。成形性把它的载体取作一位，故必须有什么东西占住那一位；hasWitnessAt 把那一位留给自己的调用方，而 hasWitness 用一个由 var zero ≐ con A 钉住的被绑定变元占住它。
这样一拆是被逼的，而理由出在消费方、不出在本章。内部层级把自己的阶段绑定起来，故可定义幂集必须在一个被绑定变元形式的载体上被描述，而集合进入公式的唯一方式是被点名为常元。于是一条点名了自己载体的谓词，在那层绑定之下压根说不出口，而这正是载体在此处不得不不再是常元的原因。钉住，是那些确实把载体握作自己一个集合的实例事后要做的事；而被钉住的形式比一般的形式长一个存在量词：那个绑定当初仅仅是为了点名那个常元而存在的。
于是哪一半难，已然定案。引入是三条早已证好的引理，施于子公式闭包。消去才是花掉元数合取项的地方，而没有它，就根本没有消去。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.CodeSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import FOL.Manipulation.Relabelling using ( mapFo ) import FOL.Absoluteness import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; tagAtL; tagAtL-adequate; closedAt ) open import L.Coding.InL {ℓ} using ( key; keyL; codeL; key∈closure ) open import L.Coding.Closed {ℓ} using ( clo; closureClosed ) open import L.Coding.Shape {ℓ} using ( shapedAt; closureShaped ) open import L.Coding.Recover {ℓ} using ( keyOf-fst; module Decode ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
是某个已言明元数处的键
一条读式，也是本章所需的唯一一件新的对象语言。元数 k 处的键，是第一分量为数码 k 的对，而标签读式对一个点了名的第二分量所说的恰是这句话。此处想要的是第二分量不点名，故这条读式就是标签读式套在一个存在量词之下，而它的两个方向就是那个存在量词的两个方向，标签读式的适足等式在里面交付。
那条等式在索引、数码与环境都还是变元时交付，因为只有这样它才便宜。下面两个调用点都在固定的索引与固定的数码上，而两者都不为那次展开付账。
keyArityAtL : ∀ {n} → Fin n → ℕ → Formula S n keyArityAtL c k = ∃̇ (tagAtL (suc c) k zero) keyArityAtL-out : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) → ⟨ γ ⊨ keyArityAtL c k ⟩ → ∥ (Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# k) (fst z))) ∥₁ keyArityAtL-out c k γ = PT.map (λ { (z , hz) → z , subst ⟨_⟩ (tagAtL-adequate (suc c) k zero (z ∷ γ)) hz }) keyArityAtL-in : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z) → ⟨ γ ⊨ keyArityAtL c k ⟩ keyArityAtL-in c k γ z e = ∣ z , subst ⟨_⟩ (sym (tagAtL-adequate (suc c) k zero (z ∷ γ))) e ∣₁
是某个元数处的键
上面那条读式把元数点名为一个元语言的数码，而正是这一点把元数钉在一上；一个必须持有诸子码的集合做不到这件事，因为量词的子公式住在高一级的元数上。故元数必须变成一个被绑定的集合，而须有什么东西对那个集合说出 # k 白送的那句话：它是一个数码。
说出它只花一个常元。ωʟ 是 L 的元素，其成员恰是诸数码，故「元数分量属于 ωʟ」就是那个条件，且写法与第二个合取项早已在用的那种无界隶属相同。两个存在量词，一个管元数、一个管载荷，中间是对读式，再加上落在元数上的那条隶属。
读回来的时候，这个选择才见分晓。ω-specL 是命题之间的等式，不是蕴含，故 ωʟ 的成员就是一个被截断的自然数，而与链的投影等式复合一次，就把它变成 recover 作为元数实参所收下的那个 # m。两个方向里都没有归纳；数码那一章已经做过了。
arityNumAtL : ∀ {n} → Fin n → Formula S n arityNumAtL c = ∃̇ (∃̇ (prAtL (suc (suc c)) (suc zero) zero ∧̇ (var (suc zero) ∈̇ con ωʟ))) arityNumAtL-out : ∀ {n} (c : Fin n) (γ : S ^ n) → ⟨ γ ⊨ arityNumAtL c ⟩ → ∥ (Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z))) ∥₁ arityNumAtL-out c γ = PT.rec squash₁ (λ { (ar , h) → PT.rec squash₁ (λ { (z , (hp , hω)) → PT.map (λ { (m , qm) → lower m , z , ( subst ⟨_⟩ (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ ar ∷ γ)) hp ∙ cong (λ w → pr w (fst z)) (qm ∙ numeralL-fst (lower m)) ) }) (subst ⟨_⟩ (ω-specL ar) hω) }) h }) arityNumAtL-in : ∀ {n} (c : Fin n) (γ : S ^ n) (m : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# m) (fst z) → ⟨ γ ⊨ arityNumAtL c ⟩ arityNumAtL-in c γ m z e = ∣ numeralL m , ∣ z , ( subst ⟨_⟩ (sym (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ numeralL m ∷ γ))) (e ∙ cong (λ w → pr w (fst z)) (sym (numeralL-fst m))) , subst ⟨_⟩ (sym (ω-specL (numeralL m))) ∣ lift m , refl ∣₁ ) ∣₁ ∣₁
那条谓词
两个合取项，落在一个自由变元上。第一项从外面钉住元数，而这正是上一章点名索取的那个合取项。第二项是解码那两条假设的见证：一个装着实参、既封闭又成形的集合。
第二项里没有任何东西是有界的，也不需要有。那个见证在引入这边由一条公式自己的子公式闭包产出，在消去那边作为 L 的一个集合被消费，而两种读法都发生在类模型处。
第二个合取项写了两遍：一遍落在两个槽位上，即载体与实参；另一遍把载体钉在一个常元上。一般的那一遍只有一个存在量词，管那个集合；被钉住的那一遍把它裹进点名 A 的那层绑定，而那层绑定就是二者之间的全部差别。下面两条谓词都逐字取用被钉住的那个形式，两条适足性的两半也都如此；分开这两条谓词的只有元数合取项，别无其他。
hasWitnessAt : ∀ {n} → Fin n → Fin n → Formula S n hasWitnessAt A x = ∃̇ ((var (suc x) ∈̇ var zero) ∧̇ (closedAt zero ∧̇ shapedAt zero (suc A))) hasWitness : S → Formula S 1 hasWitness A = ∃̇ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) isCode : S → Formula S 1 isCode A = keyArityAtL zero 1 ∧̇ hasWitness A isCodeAny : S → Formula S 1 isCodeAny A = arityNumAtL zero ∧̇ hasWitness A
那个超集，与那个集合
载体是固定的，而消费方会把它固定在某个阶段上。它的诸成员就是字母表，恰如诸编码章的两个参数所期待：到层级的嵌入，以及「它落到的东西可构造」这份证书。后者是 L 的传递性用一次，而它所施于的那条隶属关系被单独命名，因为形状谓词如今按其自身的名义索取它。
然后是那两个超集，一集一个。smallDom 索取 L 元素的一个小族，返回一个装下它全部的阶段；一元那个族以字母表之上的一元公式为索引，全元数那个族则以「一个元数连同该元数处的一条公式」之对为索引。两者都是尺寸正确的类型，因为语法是在字母表自身层级上的归纳类型，而元数是自然数，压根不花层级。回来的东西含有每个键，也含有别的许多；而分离把「别的」去掉。
两个集合都在它们被造出之处封印。不封印的话，此后每个提到其一的类型都会把分离器械的展开带进转换检查，而此处导出的诸事实已是任何消费方所需的全部。封印之内只有读分离的那几条；回来的那些方向、以及它们复合成的那些等式在封印之外，因为它们都不需要知道这个集合是从什么里切出来的。
module _ (A : S) where private ι : ⟪ fst A ⟫ → V ℓ ι = ⟪ fst A ⟫↪ ι∈ : (m : ⟪ fst A ⟫) → ⟨ ι m ∈ fst A ⟩ ι∈ m = ∈∈ₛ {a = ι m} {b = fst A} .snd (∈ₛ⟪ fst A ⟫↪ m) ιL : (m : ⟪ fst A ⟫) → ⟨ isL (ι m) ⟩ ιL m = isL-trans {x = fst A} {y = ι m} (ι∈ m) (A .snd) codeS : ∀ {n} → Formula ⟪ fst A ⟫ n → S codeS φ = VCode.⌜ mapFo ι φ ⌝ , codeL ι ιL φ keyS : ∀ {n} → Formula ⟪ fst A ⟫ n → S keyS φ = key ι ιL φ , keyL ι ιL φ private small : Σ[ d ∈ S ] ((φ : Formula ⟪ fst A ⟫ 1) → ⟨ keyS φ ∈ˢ d ⟩) small = smallDom (Formula ⟪ fst A ⟫ 1) keyS sep : isContr (SetOf (λ x → (x ∈ˢ small .fst) ⊓ ((x ∷ []) ⊨ isCode A))) sep = hasSeparationL (small .fst) (isCode A) smallAny : Σ[ d ∈ S ] ((p : Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) → ⟨ keyS (snd p) ∈ˢ d ⟩) smallAny = smallDom (Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) (λ p → keyS (snd p)) sepAny : isContr (SetOf (λ x → (x ∈ˢ smallAny .fst) ⊓ ((x ∷ []) ⊨ isCodeAny A))) sepAny = hasSeparationL (smallAny .fst) (isCodeAny A)
那个见证，进与出
第二个合取项的两半都在此处、在变元元数、变元载体位与变元环境上一次证完，而下面的一切只是把它们施用一遍。元数可以是变元，是因为那个合取项从不提它：引入为任意元数的一条公式产出一个既封闭又成形的集合，消去消费一个这样的集合并调用解码，而解码从一开始就把元数取作实参。载体与环境可以是变元，则是因为两半所倚的每条引理本来就是这样收它们的。
引入是里面什么也没有的那一半。那个见证是子公式闭包，其三笔债 key∈closure、closureClosed 与 closureShaped 各出一章，且都已偿清。其中最后一条多要一件东西，即每个常元都是载体的成员，而在这个字母表上，那正是字母表当初据以定义的那件事，沿那一位的等式搬过去即可。
消去是另一半，而它从「已以某个已言明元数处的键的形式到场的那个成员」出发，那正是 recover 所索取的、也是第二个合取项供不出的。载体那一位的等式把「属于那一位所持有的东西」变成「属于 A」，而这正是解码那条假设得以交付的原因：A 的诸成员恰是 ⟪ A ⟫ 的像，凭的是「一个集合由其自身诸成员的呈现」。读出那个存在量词，一个既封闭又成形的集合便随之到场。随后解码开跑，而它的答案是载体之上、落在它被递交的那个元数处的一条公式。
被钉住的那一对，就是这两条落在「点名那层绑定所造出的环境」上，而钉住的全部代价也就在此：引入为那层绑定供上 A、为它的等式供上 refl，消去把那层绑定读出来、再把它所持有的东西交给一般的形式。读出来的地方，正是载荷必须被点名之处。 若交给推断，被钉住的载体处那个截断的载荷就是一个元变元，代表着「一条求解器尚未认定的公式的满足关系」；同样两行，把类型写出来时两秒检查完毕，不写则跑过 140 秒并在那里被杀掉。这就是递归那条全性假设所记下的规矩，在另一处再次遇上：它不关乎那个图，它关乎在具体环境处的 PT.rec。
witnessAt-in : ∀ {n k} (b c : Fin n) (γ : S ^ n) (φ : Formula ⟪ fst A ⟫ k) → fst (lookup b γ) ≡ fst A → fst (lookup c γ) ≡ fst (keyS φ) → ⟨ γ ⊨ hasWitnessAt b c ⟩ witnessAt-in b c γ φ qb qc = ∣ clo ι ιL φ , ( subst (λ w → ⟨ w ∈ fst (clo ι ιL φ) ⟩) (sym qc) (key∈closure ι ιL φ) , ( closureClosed ι ιL φ γ , closureShaped ι ιL φ b γ (λ m → subst (λ w → ⟨ ι m ∈ w ⟩) (sym qb) (ι∈ m)) ) ) ∣₁ witnessAt-out : ∀ {n} (b c : Fin n) (γ : S ^ n) → fst (lookup b γ) ≡ fst A → ⟨ γ ⊨ hasWitnessAt b c ⟩ → (k : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z) → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁ witnessAt-out b c γ qb hw k z qz = PT.rec squash₁ viaSlot hw where Target : Type (ℓ-suc ℓ) Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁ onto : (y : V ℓ) → ⟨ y ∈ fst (lookup b γ) ⟩ → ∥ Σ[ m ∈ ⟪ fst A ⟫ ] (ι m ≡ y) ∥₁ onto y y∈ = ∣ ∈-asFiber {a = y} {b = fst A} (subst (λ w → ⟨ y ∈ w ⟩) qb y∈) ∣₁ viaSlot : Σ[ C ∈ S ] ⟨ (C ∷ γ) ⊨ ((var (suc c) ∈̇ var zero) ∧̇ (closedAt zero ∧̇ shapedAt zero (suc b))) ⟩ → Target viaSlot (C , (x∈C , (hcl , hsh))) = PT.map (λ { (ψ , qψ) → ψ , (qz ∙ cong (pr (# k)) (sym qψ)) }) (Decode.recover ι zero (suc b) (C ∷ γ) onto hcl hsh k z (subst (λ w → ⟨ w ∈ fst C ⟩) (qz ∙ sym (keyOf-fst k z)) x∈C)) private witness-in : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ (keyS φ ∷ []) ⊨ hasWitness A ⟩ witness-in φ = ∣ A , ( refl , witnessAt-in zero (suc zero) (A ∷ keyS φ ∷ []) φ refl refl ) ∣₁ witness-out : (x : S) → ⟨ (x ∷ []) ⊨ hasWitness A ⟩ → (k : ℕ) (z : S) → fst x ≡ pr (# k) (fst z) → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁ witness-out x hw k z qz = PT.rec squash₁ viaCarrier hw where viaCarrier : Σ[ B ∈ S ] ⟨ (B ∷ x ∷ []) ⊨ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) ⟩ → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁ viaCarrier (B , (qB , hB)) = witnessAt-out zero (suc zero) (B ∷ x ∷ []) qB hB k z qz
两个方向，而它们会合
两个方向所谈的那条陈述先写出来，而它是一个类：载体之上诸公式在元数一处的诸键。引入说每个这样的键都是成员，消去说每个成员都是这样一个键，故二者不再是这个集合的两道界，而是它的一条刻画。
把那个见证提出去之后，每个方向剩下的就是元数合取项。引入在 witness-in 之上添两样：属于那个超集，凭那个键所索引的族；以及元数合取项，其见证是那条码、其等式是 refl。消去先读元数合取项，因为没有它那个成员根本不以键的形式到场，再把读到的东西交给 witness-out。
IsKeyOver : S → Ω IsKeyOver x = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (fst x ≡ fst (keyS ψ))) ∥₁ , squash₁ opaque Codes : S Codes = sep .fst .fst key∈Codes : (φ : Formula ⟪ fst A ⟫ 1) → ⟨ keyS φ ∈ˢ Codes ⟩ key∈Codes φ = subst ⟨_⟩ (sym (sep .fst .snd (keyS φ))) ( small .snd φ , ( keyArityAtL-in zero 1 (keyS φ ∷ []) (codeS φ) refl , witness-in φ ) ) Codes-out : (x : S) → ⟨ x ∈ˢ Codes ⟩ → ⟨ IsKeyOver x ⟩ Codes-out x x∈ = PT.rec squash₁ (λ { (z , qz) → witness-out x (sat .snd) 1 z qz }) (keyArityAtL-out zero 1 (x ∷ []) (sat .fst)) where sat : ⟨ (x ∷ []) ⊨ isCode A ⟩ sat = subst ⟨_⟩ (sep .fst .snd x) x∈ .snd Codes-in : (x : S) → ⟨ IsKeyOver x ⟩ → ⟨ x ∈ˢ Codes ⟩ Codes-in x = PT.rec (snd (x ∈ˢ Codes)) (λ { (ψ , q) → subst (λ w → ⟨ w ∈ fst Codes ⟩) (sym q) (key∈Codes ψ) }) Codes-spec : (x : S) → (x ∈ˢ Codes) ≡ IsKeyOver x Codes-spec x = ⇔toPath (Codes-out x) (Codes-in x)
往返
两个方向如今在同一个字母表上陈述，而它们复合成一条命题之间的等式：Codes 的成员恰是载体之上某条公式的键。回来那个方向只是一次代换，因为隶属只依赖底集，而键就是一个底集；无须重证任何东西，因为 key∈Codes 早已把每个这样的键放了进去。
补上它的那个合取项是 isTmAt 的，而先前错在哪里值得明说。变元的序号有界，界自元数数码；常元的载荷则不受任何东西所界，于是那一支只说「存在某物，而载荷是它的标签」，而那个某物是 L 的任意元素。故从某个成员还原出来的公式可能点名载体之外的常元，而旧谓词的任何读法都排除不了这一点。那时这个集合被两条陈述夹住：载体之上的每条公式，其键都在里面；而每个成员回来时是模型之上的一条公式。二者不是同一类。如今是了，而全部差别就是那道对诸常元的界。
同一个集合，落在每个元数上
第二个集合与第一个只差一个合取项和一个索引类型，而它的适足性就是同样两行，只是把元数一路带着。出来的是载体之上诸公式在任意元数处的诸键之类，而那正是「对诸子码作递归」必须以之为索引的那一类，因为量词的子公式住在高一级的元数上，而一元那一类装不下它。
一元那个集合原样保留，而这个决定值得说明。它本可由旧的元数合取项从全元数集合里切出，但那样一来消去就得把「某个元数 n 处的键，且元数为一」变回元数一处的一条公式，也就是要把数码反过来求解，再沿所得的等式搬运一条公式。那比它所要替换的那次分离更费事，而两个集合早已共享了所有贵的东西：一次见证引入、一次见证消去、一次解码。
IsKeyOverAny : S → Ω IsKeyOverAny x = ∥ (Σ[ n ∈ ℕ ] Σ[ ψ ∈ Formula ⟪ fst A ⟫ n ] (fst x ≡ fst (keyS ψ))) ∥₁ , squash₁ opaque AllCodes : S AllCodes = sepAny .fst .fst key∈AllCodes : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ keyS φ ∈ˢ AllCodes ⟩ key∈AllCodes {n} φ = subst ⟨_⟩ (sym (sepAny .fst .snd (keyS φ))) ( smallAny .snd (n , φ) , ( arityNumAtL-in zero (keyS φ ∷ []) n (codeS φ) refl , witness-in φ ) ) AllCodes-out : (x : S) → ⟨ x ∈ˢ AllCodes ⟩ → ⟨ IsKeyOverAny x ⟩ AllCodes-out x x∈ = PT.rec squash₁ (λ { (k , z , qz) → PT.map (λ { (ψ , q) → k , ψ , q }) (witness-out x (sat .snd) k z qz) }) (arityNumAtL-out zero (x ∷ []) (sat .fst)) where sat : ⟨ (x ∷ []) ⊨ isCodeAny A ⟩ sat = subst ⟨_⟩ (sepAny .fst .snd x) x∈ .snd AllCodes-in : (x : S) → ⟨ IsKeyOverAny x ⟩ → ⟨ x ∈ˢ AllCodes ⟩ AllCodes-in x = PT.rec (snd (x ∈ˢ AllCodes)) (λ { (n , ψ , q) → subst (λ w → ⟨ w ∈ fst AllCodes ⟩) (sym q) (key∈AllCodes ψ) }) AllCodes-spec : (x : S) → (x ∈ˢ AllCodes) ≡ IsKeyOverAny x AllCodes-spec x = ⇔toPath (AllCodes-out x) (AllCodes-in x)
小结
两个集合，只差一条谓词。Codes 是 L 的元素，凭 Codes-spec，它的诸成员恰是载体之上诸公式在元数一处的诸键；那正是可定义幂集所需要的那条陈述，因为 Def A 以那一类、而非别的任何一类为索引。AllCodes 是同一套构造，只是元数由点名改为绑定，而 AllCodes-spec 把它钉在每个元数处的诸键上。
全部内容在两个合取项里，而两者同类。封闭性与成形性合起来认出的是码的形状，对一个键所携带的元数、以及它的诸常元出自哪个字母表，都只字未提，故一条对着它们写下的解码必须被递交这两样，而一个由它们造出的集合必须把这两样说出来。smallDom 与任意公式的分离做掉其余，而两者都没有索取前几章尚未付清的任何东西。
全元数那个集合的存在，是为了它所刻画的那一类，而不是为了某条关于它的定理。对码的递归必须在一个码的诸子码处作答，而量词的子公式住在高一级的元数上，一元那一类装不下它，故定义域只能是每个元数处的诸键。元数合取项所改的那件事，即从元语言的数码改为属于 ωʟ，就是「递归可以据以索引的集合」与「递归不可据以索引的集合」之间的全部差别。