Bedrock可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。
交互式目录 · 依赖图固定宇宙层级 ℓ。保留这个层级参数，使构造可以在所需的各个大小处实例化，而不必把不同的宇宙视为同一个。
module L.Coding.FormulaRecovery {ℓ : Level} where
形状正确且对子码封闭的键集合应当包含真正的公式码。给定一个元数为指定自然数的键，本章证明它编码了一条常元取自指定载体的公式。证明对码的秩作归纳，所得结论是所恢复公式的仅仅存在性。
那条公式落在哪个字母表上，是整章的要害，而它在此处定案，而不在末尾。模型之上的公式会由同样六个框架还原出来，而对消费方毫无用处，因为它的索引类型是单个载体之上的诸公式。故目标在一个字母表上陈述，字母表是一个参数，而关于它的、形状谓词供不出的那一件事，即载体的诸元素就是字母表的像，作为一条假设摆在旁边。
目标采用字母表自身的编码，这使各框架更短。在模型上，每个框架都必须先对应模型编码与层级编码，才能比较一个码和一个载荷；在字母表上，码本来就是层级的元素，因此不需要这层对应。
此处没有证明的是「每个元素都是这样一个键」，而欠这笔账的是那个集合。形状把元数分量存在量化、且对它不加任何条件，故一个持有「第一分量不是数码的对」的集合同样满足两半，而本定理对它什么也没说。下一章所造的那个集合从外面把元数钉住，即在一个固定元数上被索引的族之内作分离，这正是不去要求那条谓词的原因。
递归跑在码的秩上，不跑在码上、也不跑在键上。不跑在码上，是因为成员关系不下降进 Kuratowski 的对；不跑在键上，是因为键在码旁边还带着元数，而「对的秩的算术」是一条没人证过的事实。把元数作为一个自然数在旁边带着、只对码下降，两者都不需要。
一步是 peel，一次下降是上一章，而十个情形收拢为六个，因为十个标签之间只有六种形状，而一种形状之内变动的只是一个标签与一个构造子。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
using ( module InfinitySet )
open InfinitySet using ( #_; sucV )
open hPropView 𝒮ʟ
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
键与解码命题
一个键由元数与码配对而成。解码要求存在字母表 K 上具有该元数的公式，将其常元映入层级后，所得编码正是给定的码。命题截断记录这样一条公式的存在，而不选定具体代表。
码是对该公式在层级中的像取的，那正是 mapFo 在那里做的事。它不是构造的一步：常元改名按定义与每个构造子交换，故字母表之上的一条公式连同它的像，其编码与模型之上的公式完全一样。
keyOf : ℕ → S → S
keyOf n x = prʟ (numeralL n) x
keyOf-fst : (n : ℕ) (x : S) → (keyOf n x) .fst ≡ pr (# n) (x .fst)
keyOf-fst n x = prʟ-fst (numeralL n) x ∙ cong₂ pr (numeralL-fst n) refl
Coded : {K : Type ℓ} (f : K → V ℓ) → ℕ → S → Type (ℓ-suc ℓ)
Coded {K} f n x = ∥ Σ[ φ ∶ Formula K n ] (VCode.⌜ mapFo f φ ⌝ ≡ x .fst) ∥₁
对码的秩作归纳
封闭性提供直接子公式的键，而它们的秩严格更小。因此，秩归纳允许先解码子公式，再重建整条公式。归纳命题允许元数变化，从而也能处理量词。
字母表的两个参数出于同样的理由骑在归纳之外。六个框架里只有两个去看它们，即载荷里放着词项的那两个，而它们看的方式，是把那条假设径直递给词项解码。
module Decode {K : Type ℓ} (f : K → V ℓ)
{m : ℕ} (C A : Fin m) (γ : Vec S m) (onto : Onto f A γ)
(hcl : ⟨ γ ⊨ closedAt C ⟩) (hsh : ⟨ γ ⊨ shapedAt C A ⟩) where
open Peel C A γ hcl hsh
Wf : ℕ → S → Type (ℓ-suc ℓ)
Wf n x = ⟨ keyOf n x ∈ˢ lookup C γ ⟩
recover : (n : ℕ) (x : S) → Wf n x → Coded f n x
recover n x = ∈-induction go (rank (x .fst)) n x refl
where
P : V ℓ → Type (ℓ-suc ℓ)
P r = (j : ℕ) (z : S) → rank (z .fst) ≡ r → Wf j z → Coded f j z
go : (r : V ℓ) → ((y : V ℓ) → ⟨ y ∈ r ⟩ → P y) → P r
go r IH j z qr wz = rec₁ squash₁ fill (peel (keyOf j z) wz)
where
D = (lookup C γ) .fst
rec : (i : ℕ) (u : S) → ⟨ rank (u .fst) ∈ rank (z .fst) ⟩
→ Wf i u → Coded f i u
rec i u lt wu = IH (rank (u .fst))
(subst (λ w → ⟨ rank (u .fst) ∈ w ⟩) qr lt) i u refl wu
英文原文
The arity numeral and the payload, read out of the key's shape.
split : (N : S) (p : V ℓ) → (keyOf j z) .fst ≡ pr (N .fst) p
→ (# j ≡ N .fst) × (z .fst ≡ p)
split N p e = pr-inj (sym (keyOf-fst j z) ∙ e)
inD : (i : ℕ) (N u : S) → # i ≡ N .fst → ⟨ pr (N .fst) (u .fst) ∈ D ⟩
→ Wf i u
inD i N u qN h = subst (λ w → ⟨ w ∈ D ⟩)
(cong₂ pr (sym qN) refl ∙ sym (keyOf-fst i u)) h
inD⁺ : (i : ℕ) (N u : S) → # i ≡ N .fst
→ ⟨ pr (sucV (N .fst)) (u .fst) ∈ D ⟩ → Wf (suc i) u
inD⁺ i N u qN h = subst (λ w → ⟨ w ∈ D ⟩)
(cong₂ pr (cong sucV (sym qN)) refl ∙ sym (keyOf-fst (suc i) u)) h
英文原文
The six frames. Each takes the constructor's coding equation rather than leaving the elaborator to find it: with the constructor a variable, nothing reduces, and the unification is the whole cost. Over the alphabet the equation is still refl at every call site, because relabelling commutes with every constructor definitionally.
atom : (k : ℕ) (op : ∀ {i} → Term K i → Term K i → Formula K i)
→ (∀ {i} (t u : Term K i)
→ VCode.⌜ mapFo f (op t u) ⌝
≡ VCode.mkTag k (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ))
→ BinWit k (bothTm A) γ (keyOf j z) → Coded f j z
atom k op qop (N , (a , (b , (e , (ha , hb))))) =
rec₁ squash₁
(λ { (t , qt) → map₁
(λ { (u , qu) → op t u
, ( qop t u
∙ cong (VCode.mkTag k) (cong₂ pr qt qu)
∙ sym qx ) })
(isTmAt-decode f zero (suc (suc zero)) (suc (suc (suc (suc A))))
(b ∷ a ∷ N ∷ keyOf j z ∷ γ) j (sym qN) onto hb) })
(isTmAt-decode f (suc zero) (suc (suc zero)) (suc (suc (suc (suc A))))
(b ∷ a ∷ N ∷ keyOf j z ∷ γ) j (sym qN) onto ha)
where
sp = split N (pr (# k) (pr (a .fst) (b .fst))) e
qN = sp .fst
qx = sp .snd
binSame : (k : ℕ) (op : ∀ {i} → Formula K i → Formula K i → Formula K i)
→ (∀ {i} (φ ψ : Formula K i)
→ VCode.⌜ mapFo f (op φ ψ) ⌝
≡ VCode.mkTag k (pr VCode.⌜ mapFo f φ ⌝ VCode.⌜ mapFo f ψ ⌝))
→ BinSame k (keyOf j z) → Coded f j z
binSame k op qop (N , (a , (b , (e , (ha , hb))))) =
rec₁ squash₁
(λ { (φ , qφ) → map₁
(λ { (ψ , qψ) → op φ ψ
, ( qop φ ψ
∙ cong (VCode.mkTag k) (cong₂ pr qφ qψ)
∙ sym qx ) })
(rec j b (subst (λ w → ⟨ rank (b .fst) ∈ rank w ⟩) (sym qx)
(rightPart (# k) (a .fst) (b .fst)))
(inD j N b qN hb)) })
(rec j a (subst (λ w → ⟨ rank (a .fst) ∈ rank w ⟩) (sym qx)
(leftPart (# k) (a .fst) (b .fst)))
(inD j N a qN ha))
where
sp = split N (pr (# k) (pr (a .fst) (b .fst))) e
qN = sp .fst
qx = sp .snd
unSame : (k : ℕ) (op : ∀ {i} → Formula K i → Formula K i)
→ (∀ {i} (φ : Formula K i)
→ VCode.⌜ mapFo f (op φ) ⌝ ≡ VCode.mkTag k VCode.⌜ mapFo f φ ⌝)
→ UnSame k (keyOf j z) → Coded f j z
unSame k op qop (N , (a , (e , ha))) = map₁
(λ { (φ , qφ) → op φ
, ( qop φ ∙ cong (VCode.mkTag k) qφ ∙ sym qx ) })
(rec j a (subst (λ w → ⟨ rank (a .fst) ∈ rank w ⟩) (sym qx)
(payload≺ (# k) (a .fst)))
(inD j N a qN ha))
where
sp = split N (pr (# k) (a .fst)) e
qN = sp .fst
qx = sp .snd
konst : (k : ℕ) (op : ∀ {i} → Formula K i)
→ (∀ i → VCode.⌜ mapFo f (op {i}) ⌝ ≡ VCode.mkTag k (# 0))
→ UnWit k zeroPay γ (keyOf j z) → Coded f j z
konst k op qop (N , (a , (e , ha))) = ∣ op
, ( qop j ∙ cong (VCode.mkTag k) (sym (ha ∙ numeralL-fst 0))
∙ sym qx ) ∣₁
where
qx = split N (pr (# k) (a .fst)) e .snd
unSucc : (k : ℕ) (op : ∀ {i} → Formula K (suc i) → Formula K i)
→ (∀ {i} (φ : Formula K (suc i))
→ VCode.⌜ mapFo f (op φ) ⌝ ≡ VCode.mkTag k VCode.⌜ mapFo f φ ⌝)
→ UnSucc k (keyOf j z) → Coded f j z
unSucc k op qop (N , (a , (e , ha))) = map₁
(λ { (φ , qφ) → op φ
, ( qop φ ∙ cong (VCode.mkTag k) qφ ∙ sym qx ) })
(rec (suc j) a
(subst (λ w → ⟨ rank (a .fst) ∈ rank w ⟩) (sym qx)
(payload≺ (# k) (a .fst)))
(inD⁺ j N a qN ha))
where
sp = split N (pr (# k) (a .fst)) e
qN = sp .fst
qx = sp .snd
bnd : (k : ℕ) (op : ∀ {i} → Term K i → Formula K (suc i) → Formula K i)
→ (∀ {i} (t : Term K i) (φ : Formula K (suc i))
→ VCode.⌜ mapFo f (op t φ) ⌝
≡ VCode.mkTag k (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f φ ⌝))
→ BinSucc k (keyOf j z) → Coded f j z
bnd k op qop (N , (a , (b , (e , (ha , hb))))) =
rec₁ squash₁
(λ { (t , qt) → map₁
(λ { (φ , qφ) → op t φ
, ( qop t φ
∙ cong (VCode.mkTag k) (cong₂ pr qt qφ)
∙ sym qx ) })
(rec (suc j) b (subst (λ w → ⟨ rank (b .fst) ∈ rank w ⟩) (sym qx)
(rightPart (# k) (a .fst) (b .fst)))
(inD⁺ j N b qN hb)) })
(isTmAt-decode f zero (suc zero) (suc (suc (suc A)))
(a ∷ N ∷ keyOf j z ∷ γ) j (sym qN) onto ha)
where
sp = split N (pr (# k) (pr (a .fst) (b .fst))) e
qN = sp .fst
qx = sp .snd
fill : PeelWit (keyOf j z) → Coded f j z
fill =
⊎-rec (atom 0 _∈̇_ (λ _ _ → refl))
(⊎-rec (atom 1 _≐_ (λ _ _ → refl))
(⊎-rec (binSame 2 _∧̇_ (λ _ _ → refl))
(⊎-rec (binSame 3 _∨̇_ (λ _ _ → refl))
(⊎-rec (binSame 4 _⇒̇_ (λ _ _ → refl))
(⊎-rec (konst 5 ⊥̇ (λ _ → refl))
(⊎-rec (unSucc 6 ∃̇_ (λ _ → refl))
(⊎-rec (unSucc 7 ∀̇_ (λ _ → refl))
(⊎-rec (bnd 8 ∀̇∈ (λ _ _ → refl))
(bnd 9 ∃̇∈ (λ _ _ → refl))))))))))