BedrockWell-formed keys
「是一个码」中封闭性没有说出的那一半。
closedAt 是八条以标签为键的蕴含：若某个成员带这个标签，则它的诸部件也是成员。那里没有任何东西排除掉「压根没有可辨标签」的成员，而这样的成员平凡地满足全部八条。故一个封闭集可以含有垃圾，而说出相反之事的谓词就是这一条：每个成员都是一个带元数标签的对，其标签属于那十二个之一，且载荷具有该标签所要求的形状。
四个叶子标签交给一个参数。它们的载荷提到的是词项码与一个数码、从不提公式码，故它们身上没有任何东西会下降，也没有任何东西属于同一场归纳；它们在别处写一次，然后递进来。
成形性是在两位上陈述的，不是一位：那个集合，以及其中诸词项从中取常元的一个载体。第二位使一个成员成为该载体之上某条公式的键、而非整个模型之上的，而它正是码集当初被两条陈述夹住时所缺的那个合取项。它写作一位、而非一个常元，于是被穿过下面的一切，且不重新索引任何东西。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth module L.Coding.Shape {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇ ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.Manipulation.Relabelling using ( mapTm; mapFo ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; #mono; module VCode ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; sucV ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( tagAtL; tagAtL-adequate ; closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt ; oneSuccAt; succSndAt ; binSameClosed-out; unSameClosed-out ; unSuccClosed-out; binSuccClosed-out ; arityTagAtL; arityTagAtL-adequate ; arityTagPairAtL; arityTagPairAtL-adequate; numL ) open import L.Coding.InL {ℓ} using ( closure-inv; key; codeL; codeTmL ) open import L.Coding.Closed {ℓ} using ( clo ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Ordinal {ℓ} using ( ∈#-elim ) open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.FinData.Properties using ( fromℕ'; toFromId'; toℕ<n ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Data.Unit using ( tt* ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
两个载荷框架
一类标签的载荷是一个对，另一类的载荷是单个码。十二个标签，两种形状：标签取哪一种是唯一变动的东西，而它对载荷的其余要求，是框架所携带的一条关系。这与封闭性谓词所作的划分相同，理由也相同。
module _ {n : ℕ} where binForm : ℕ → Formula S (4 + n) → Formula S (suc n) binForm k rel = ∃̇ (∃̇ (∃̇ (arityTagPairAtL (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero ∧̇ rel))) unForm : ℕ → Formula S (3 + n) → Formula S (suc n) unForm k rel = ∃̇ (∃̇ (arityTagAtL (suc (suc zero)) (suc zero) k zero ∧̇ rel))
词项码
那四个载荷伸到公式码之外的标签，需要一条谓词，而它不是递归的：词项要么是常元、要么是变元，二者都没有部件。两支都有界，而界住它们的不是同一样东西。
变元的序号必须落在元数之下，正是这一点使那条公式成为在该元数上的词项之码、而非在某个更大的元数上。常元则必须是载体的成员，正是这一点使它成为在该字母表之上的词项之码、而非在整个模型之上。第二个合取项，正是码集当初被两条陈述夹住时所缺的那一个：常元一旦不受界，一个被读回作常元的载荷就是 L 的任意元素，而解码落进的那一类，就比引入出发的那一类更宽。
两道界都是「某一位上的成员关系」，两位都由调用方点名。载体取一位、而不取一个常元，是有意为之。常元会把这条线以下的每条谓词钉死在一个载体上，而以它们为索引的一切都将在那个对上重新索引；一位是被穿过去的，而穿过去不花钱。
isTmAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n isTmAt t N A = ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A))) ∨̇ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N)))
十二条，作为一条谓词
每个成员都是一个良构的键：一个带元数标签的对，携带那十二个标签之一，且载荷是该标签所要求的那种。诸关系说出封闭性没有说的事：原子的两个部件是词项码、有界量词的第一个部件是词项码、常元的载荷是零。公式部件留给封闭性，那也正是它们该在的地方，因为它们是唯一有东西会下降进去的部件。
于是「成形」相对的是两位、而非一位：那个集合，以及它的诸词项从中点名常元的那个载体。只有那四条提到词项的关系去看第二位，而它们也是仅有的四条能去看的。
module _ {n : ℕ} where bothTm fstTm : Fin n → Formula S (4 + n) bothTm A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A)))) ∧̇ isTmAt zero (suc (suc zero)) (suc (suc (suc (suc A)))) fstTm A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A)))) noneB : Formula S (4 + n) noneB = ⊤̇ {n = 4 + n} zeroPay noneU : Formula S (3 + n) zeroPay = var zero ≐ con (numeralL 0) noneU = ⊤̇ {n = 3 + n} shapes : Fin n → Formula S (suc n) shapes A = binForm 0 (bothTm A) ∨̇ (binForm 1 (bothTm A) ∨̇ (binForm 2 noneB ∨̇ (binForm 3 noneB ∨̇ (binForm 4 noneB ∨̇ (unForm 5 noneU ∨̇ (unForm 6 zeroPay ∨̇ (unForm 7 zeroPay ∨̇ (unForm 8 noneU ∨̇ (unForm 9 noneU ∨̇ (binForm 10 (fstTm A) ∨̇ binForm 11 (fstTm A))))))))))) shapedAt : Fin n → Fin n → Formula S n shapedAt C A = ∀̇∈ (var C) (shapes A)
一个成员是什么，摊平来读
十二个可能。两个框架各读一次，且对它们所携带的关系泛型，好让下面那趟走过析取的路是两条读式的十二次施用，而不是同一段解嵌套的十二份拷贝。
BinWit : ∀ {n} → ℕ → Formula S (4 + n) → S ^ n → S → Type (ℓ-suc ℓ) BinWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b)))) × ⟨ (b ∷ a ∷ N ∷ c ∷ γ) ⊨ rel ⟩))) UnWit : ∀ {n} → ℕ → Formula S (3 + n) → S ^ n → S → Type (ℓ-suc ℓ) UnWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ (a ∷ N ∷ c ∷ γ) ⊨ rel ⟩)) binForm-out : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S) → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩ → ∥ BinWit k rel γ c ∥₁ binForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) → PT.rec squash₁ (λ { (a , ha) → PT.map (λ { (b , (hb , hr)) → N , (a , (b , (subst ⟨_⟩ (arityTagPairAtL-adequate (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero (b ∷ a ∷ N ∷ c ∷ γ)) hb , hr))) }) ha }) hN }) unForm-out : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S) → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩ → ∥ UnWit k rel γ c ∥₁ unForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) → PT.map (λ { (a , (ha , hr)) → N , (a , (subst ⟨_⟩ (arityTagAtL-adequate (suc (suc zero)) (suc zero) k zero (a ∷ N ∷ c ∷ γ)) ha , hr)) }) hN }) ShapeWit : ∀ {n} → Fin n → S ^ n → S → Type (ℓ-suc ℓ) ShapeWit A γ c = BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c ⊎ (BinWit 2 noneB γ c ⊎ (BinWit 3 noneB γ c ⊎ (BinWit 4 noneB γ c ⊎ (UnWit 5 noneU γ c ⊎ (UnWit 6 zeroPay γ c ⊎ (UnWit 7 zeroPay γ c ⊎ (UnWit 8 noneU γ c ⊎ (UnWit 9 noneU γ c ⊎ (BinWit 10 (fstTm A) γ c ⊎ BinWit 11 (fstTm A) γ c)))))))))) shaped-out : ∀ {n} (C A : Fin n) (γ : S ^ n) → ⟨ γ ⊨ shapedAt C A ⟩ → (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁ shaped-out C A γ h c c∈ = d1 (h c c∈) where d11 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 10 (fstTm A) γ c x) ; (inr x) → PT.map inr (binForm-out 11 (fstTm A) γ c x) }) d10 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 9 noneU γ c x) ; (inr x) → PT.map inr (d11 x) }) d9 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 8 noneU γ c x) ; (inr x) → PT.map inr (d10 x) }) d8 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 7 zeroPay γ c x) ; (inr x) → PT.map inr (d9 x) }) d7 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 6 zeroPay γ c x) ; (inr x) → PT.map inr (d8 x) }) d6 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 5 noneU γ c x) ; (inr x) → PT.map inr (d7 x) }) d5 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 4 noneB γ c x) ; (inr x) → PT.map inr (d6 x) }) d4 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 3 noneB γ c x) ; (inr x) → PT.map inr (d5 x) }) d3 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 2 noneB γ c x) ; (inr x) → PT.map inr (d4 x) }) d2 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 1 (bothTm A) γ c x) ; (inr x) → PT.map inr (d3 x) }) d1 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 0 (bothTm A) γ c x) ; (inr x) → PT.map inr (d2 x) })
同样的十二条，写出来
一条为了被消费而写下的谓词，在有东西满足它之前什么也没证明。解码把「成形的集合」作为假设收下，故供给那个集合的人欠着那条假设，而欠着它意味着要造：存在式的框架有它的诸见证要产出、一个析取支要选定，而消去那边只需把它们拆开。
两个框架各引入一次，且对关系泛型，理由与决定消去的那个相同，另加一个。每个框架所携带的适足等式在此处交付，其时标签、关系与环境都还是变元。若改在一个点了名的标签处交付，那就是把一条嵌套三层量词的公式展开十二遍，而那是一秒与一下午的差别。
binForm-in : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S) → BinWit k rel γ c → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩ binForm-in k rel γ c (N , (a , (b , (e , hr)))) = ∣ N , ∣ a , ∣ b , (subst ⟨_⟩ (sym (arityTagPairAtL-adequate (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero (b ∷ a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁ ∣₁ unForm-in : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S) → UnWit k rel γ c → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩ unForm-in k rel γ c (N , (a , (e , hr))) = ∣ N , ∣ a , (subst ⟨_⟩ (sym (arityTagAtL-adequate (suc (suc zero)) (suc zero) k zero (a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁
走过那个析取的路，是读它那趟路的镜像：十二次注入一条右嵌套的链，而每一层各自带一个截断，因为真值代数的析取是一个被截断的和。诸注入是写开的，而不是命名的，因为一条对两个析取支泛型的引理，将不得不从一个已经展开了的目标里把它们找回来，而再多的合一也无法从一条公式的含义里把那条公式找回来。调用者最后欠的，对每个成员恰好是一件事：那个成员是十二者中的哪一个。
shaped-in : ∀ {n} (C A : Fin n) (γ : S ^ n) → ((c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁) → ⟨ γ ⊨ shapedAt C A ⟩ shaped-in C A γ g c c∈ = PT.rec (snd ((c ∷ γ) ⊨ shapes A)) fill (g c c∈) where fill : ShapeWit A γ c → ⟨ (c ∷ γ) ⊨ shapes A ⟩ fill (inl x) = ∣ inl (binForm-in 0 (bothTm A) γ c x) ∣₁ fill (inr (inl x)) = ∣ inr ∣ inl (binForm-in 1 (bothTm A) γ c x) ∣₁ ∣₁ fill (inr (inr (inl x))) = ∣ inr ∣ inr ∣ inl (binForm-in 2 noneB γ c x) ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inl x)))) = ∣ inr ∣ inr ∣ inr ∣ inl (binForm-in 3 noneB γ c x) ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inl x))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (binForm-in 4 noneB γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inl x)))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 5 noneU γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inl x))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 6 zeroPay γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inl x)))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 7 zeroPay γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 8 noneU γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x)))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 9 noneU γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (binForm-in 10 (fstTm A) γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr x))))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr (binForm-in 11 (fstTm A) γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
词项，被还原
第一个解码，也是唯一一个不需要归纳的。词项要么是常元、要么是变元：常元那支把载荷读回作字母表的一个常元，变元那支从元数数码里读出一个序号。每一支恰好花掉它那个析取项所携带的那道界，而两支都不能在没有界的情况下写出来。此处没有任何东西下降，这既是它可以从随后那场递归里分离出来的原因，也是它被先写下来的原因。
词项是在什么之上被造出来的，这是一个参数，而这正是本章的用处所在。字母表是任何带有到层级之嵌入的类型，而常元那支需要一样形状谓词供不出的东西：载体的诸成员就是字母表的像。那是一条假设，因为它是关于「字母表与载体」这一对的事实，而不是关于码的事实。在唯一要紧的那个实例处，字母表就是载体自己的成员类型，而这条假设就是「一个集合由其诸成员的呈现」，故它的代价是一次交付、而非一次构造。
两个析取支由两条点了名的引理去读，而那条读式就是它们的分情形，这不是趣味问题。写成一个函数的两条子句时，每支各带一个截断、而它们所在的析取自己也带一个，本章十分钟内没跑完；把每支的读法各给一个写出来的类型之后，两秒不到就查完。这条规矩是归约器的、不是数学的：类型被写出来的分支对着那个类型求解，类型靠推断的分支对着整个析取求解。
module _ {K : Type ℓ} (f : K → V ℓ) where TmWit : ℕ → V ℓ → Type (ℓ-suc ℓ) TmWit n x = Σ[ t ∈ Term K n ] (VCode.⌜ mapTm f t ⌝ᵗ ≡ x) Onto : ∀ {m} → Fin m → S ^ m → Type (ℓ-suc ℓ) Onto A γ = (y : V ℓ) → ⟨ y ∈ fst (lookup A γ) ⟩ → ∥ Σ[ c ∈ K ] (f c ≡ y) ∥₁ tmCon : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → Onto A γ → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A))) ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁ tmCon t N A γ n onto = PT.rec squash₁ (λ { (y , (hy , y∈)) → PT.map (λ { (c , qc) → con c , ( cong (VCode.mkTag 0) qc ∙ sym (subst ⟨_⟩ (tagAtL-adequate (suc t) 0 zero (y ∷ γ)) hy) ) }) (onto (fst y) y∈) }) tmVar : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → fst (lookup N γ) ≡ # n → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N))) ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁ tmVar t N A γ n qN = PT.rec squash₁ (λ { (z , (hz , z∈)) → PT.map (λ { (j , (j<n , ez)) → var (fromℕ' n j j<n) , ( cong (VCode.mkTag 1) (cong #_ (toFromId' n j j<n) ∙ sym ez) ∙ sym (subst ⟨_⟩ (tagAtL-adequate (suc t) 1 zero (z ∷ γ)) hz) ) }) (∈#-elim n (fst z) (subst (λ w → ⟨ fst z ∈ w ⟩) qN z∈)) }) isTmAt-decode : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → fst (lookup N γ) ≡ # n → Onto A γ → ⟨ γ ⊨ isTmAt t N A ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁ isTmAt-decode t N A γ n qN onto = PT.rec squash₁ (λ { (inl h) → tmCon t N A γ n onto h ; (inr h) → tmVar t N A γ n qN h })
词项，被编码
同样的两支反过来读，也是引入这一半里唯一需要算点什么、而不只是重新包装的地方。如今每一支除标签等式外还欠着自己那道界，而两笔债欠给不同的人。常元就是自己的码，故它的标签等式什么也不是，它所欠的是「该常元是载体的成员」：此处这是一条假设，因为只有调用方知道它指的是哪个载体。变元则要把它的序号放进元数数码里，这是另一道界朝着它被设计的方向出力：解码从一个数码里读出一个序号，此处则表明一个数码含有一个序号。第二件事早已在手，因为「较小的数码属于较大的」正是使相异的数码成其为相异的那件事。
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where isTmAt-in : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → fst (lookup N γ) ≡ # n → ((c : K) → ⟨ f c ∈ fst (lookup A γ) ⟩) → TmWit f n (fst (lookup t γ)) → ⟨ γ ⊨ isTmAt t N A ⟩ isTmAt-in t N A γ n qN into (con c , e) = ∣ inl ∣ y , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 0 zero (y ∷ γ))) (sym e) , into c ) ∣₁ ∣₁ where y : S y = f c , h c isTmAt-in t N A γ n qN into (var i , e) = ∣ inr ∣ z , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 1 zero (z ∷ γ))) (sym e ∙ cong (VCode.mkTag 1) (sym (numeralL-fst (toℕ i)))) , subst (λ w → ⟨ fst z ∈ w ⟩) (sym qN) (subst (λ w → ⟨ w ∈ (# n) ⟩) (sym (numeralL-fst (toℕ i))) (#mono (toℕ i) n (toℕ<n i))) ) ∣₁ ∣₁ where z : S z = numeralL (toℕ i)
剥掉一层
两半会合。形状说出一个成员是十二者中的哪一个，并把它的部件交回；封闭性说那些部件也是成员，且在该标签所要求的元数上。两半各自都给不出递归的一步，合起来恰好给出一步。
形状产出的那条等式，正是封闭性所消费的那一条，逐字相同，故二者之间无需任何东西即可复合。这不是运气：两者都是对着「带元数标签的对」的同一条读法写下的。
module Peel {m : ℕ} (C A : Fin m) (γ : S ^ m) (hcl : ⟨ γ ⊨ closedAt C ⟩) (hsh : ⟨ γ ⊨ shapedAt C A ⟩) where private D : V ℓ D = fst (lookup C γ) BinSame BinSucc : ℕ → S → Type (ℓ-suc ℓ) BinSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b)))) × (⟨ pr (fst N) (fst a) ∈ D ⟩ × ⟨ pr (fst N) (fst b) ∈ D ⟩)))) BinSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b)))) × (⟨ (a ∷ N ∷ c ∷ γ) ⊨ isTmAt zero (suc zero) (suc (suc (suc A))) ⟩ × ⟨ pr (sucV (fst N)) (fst b) ∈ D ⟩)))) UnSame UnSucc : ℕ → S → Type (ℓ-suc ℓ) UnSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (fst N) (fst a) ∈ D ⟩)) UnSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (sucV (fst N)) (fst a) ∈ D ⟩)) PeelWit : S → Type (ℓ-suc ℓ) PeelWit c = BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c ⊎ (BinSame 2 c ⊎ (BinSame 3 c ⊎ (BinSame 4 c ⊎ (UnSame 5 c ⊎ (UnWit 6 zeroPay γ c ⊎ (UnWit 7 zeroPay γ c ⊎ (UnSucc 8 c ⊎ (UnSucc 9 c ⊎ (BinSucc 10 c ⊎ BinSucc 11 c)))))))))) peel : (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ PeelWit c ∥₁ peel c c∈ = PT.map fill (shaped-out C A γ hsh c c∈) where bs : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩ → BinWit k noneB γ c → BinSame k c bs k h (N , (a , (b , (e , _)))) = N , (a , (b , (e , binSameClosed-out C k γ h c N a b c∈ e))) us : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩ → UnWit k noneU γ c → UnSame k c us k h (N , (a , (e , _))) = N , (a , (e , unSameClosed-out C k γ h c N a c∈ e)) uz : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → UnWit k noneU γ c → UnSucc k c uz k h (N , (a , (e , _))) = N , (a , (e , unSuccClosed-out C k γ h c N a c∈ e)) bz : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → BinWit k (fstTm A) γ c → BinSucc k c bz k h (N , (a , (b , (e , hr)))) = N , (a , (b , (e , (hr , binSuccClosed-out C k γ h c N a b c∈ e)))) fill : ShapeWit A γ c → PeelWit c fill (inl x) = inl x fill (inr (inl x)) = inr (inl x) fill (inr (inr (inl x))) = inr (inr (inl (bs 2 (hcl .fst) x))) fill (inr (inr (inr (inl x)))) = inr (inr (inr (inl (bs 3 (hcl .snd .fst) x)))) fill (inr (inr (inr (inr (inl x))))) = inr (inr (inr (inr (inl (bs 4 (hcl .snd .snd .fst) x))))) fill (inr (inr (inr (inr (inr (inl x)))))) = inr (inr (inr (inr (inr (inl (us 5 (hcl .snd .snd .snd .fst) x)))))) fill (inr (inr (inr (inr (inr (inr (inl x))))))) = inr (inr (inr (inr (inr (inr (inl x)))))) fill (inr (inr (inr (inr (inr (inr (inr (inl x)))))))) = inr (inr (inr (inr (inr (inr (inr (inl x))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inl (uz 8 (hcl .snd .snd .snd .snd .fst) x))))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x)))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (uz 9 (hcl .snd .snd .snd .snd .snd .fst) x)))))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (bz 10 (hcl .snd .snd .snd .snd .snd .snd .fst) x))))))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr x))))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (bz 11 (hcl .snd .snd .snd .snd .snd .snd .snd) x)))))))))))
闭包是成形的
这条谓词是干什么用的。对码的递归收到一个索引集，而那个集合必须封闭，否则诸子句什么也约束不了；也必须成形，否则它们放垃圾进来。封闭性在一章之前已为闭包交付；这里是另一半，而且是较短的那一半，因为成形性对「一个成员随身拖进什么」不作任何要求。于是那个反演返回的东西有一半被丢在地上。
分情形只对构造子进行。标签不是要与之对上的第二个索引：它由构造子算出，正如 byTag 从构造子算出封闭性的要求，故这张表是十二行、而不是十二乘十二。此处也没有任何递归，因为一个点了名的构造子之键，已经算成了见证类型所索取的那个带元数标签的对，而那十二个元组里任何地方都不需要搬运。
元组唯一算不出来的是词项见证：载荷位上放着的词项码必须被认证为词项码，而那份认证就是上面那条编码式施于该构造子所携的词项。这份认证如今有了第二半，而由调用方支付：字母表的每个常元都是载体的成员。它是一条假设，每次调用交付一次、而不是每个构造子交付一次，因为字母表是在公式之前就固定下来的。
另一方面，第一半变便宜了。一个词项所欠的见证是「它的码是某个词项的码」，而在字母表之上，一个词项的码本来就是这个：编码式就是恒等，旁边配一个 refl。在模型自己的编码上，它先得把两套编码搭起桥来。
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where private cd : ∀ {n} → Formula K n → S cd φ = VCode.⌜ mapFo f φ ⌝ , codeL f h φ ct : ∀ {n} → Term K n → S ct t = VCode.⌜ mapTm f t ⌝ᵗ , codeTmL f h t nn : ℕ → S nn n = # n , numL n tw : ∀ {n} (t : Term K n) → TmWit f n (fst (ct t)) tw t = t , refl closureShaped : ∀ {n m} (φ : Formula K n) (A : Fin m) (γ : S ^ m) → ((k : K) → ⟨ f k ∈ fst (lookup A γ) ⟩) → ⟨ (clo f h φ ∷ γ) ⊨ shapedAt zero (suc A) ⟩ closureShaped φ A γ into = shaped-in zero (suc A) (clo f h φ ∷ γ) (λ c c∈ → PT.map (λ { (_ , ψ , q , _) → go ψ c q }) (closure-inv f h φ (fst c) c∈)) where tm1 : ∀ {k} (t : Term K k) (b c : S) → ⟨ (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ) ⊨ isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc (suc A))))) ⟩ tm1 {k} t b c = isTmAt-in f h (suc zero) (suc (suc zero)) (suc (suc (suc (suc (suc A))))) (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw t) tm0 : ∀ {k} (u : Term K k) (a c : S) → ⟨ (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ) ⊨ isTmAt zero (suc (suc zero)) (suc (suc (suc (suc (suc A))))) ⟩ tm0 {k} u a c = isTmAt-in f h zero (suc (suc zero)) (suc (suc (suc (suc (suc A))))) (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw u) go : ∀ {k} (ψ : Formula K k) (c : S) → fst c ≡ key f h ψ → ShapeWit (suc A) (clo f h φ ∷ γ) c go {k} (t ∈̇ u) c q = inl (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c))))) go {k} (t ≐ u) c q = inr (inl (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c)))))) go {k} (a ∧̇ b) c q = inr (inr (inl (nn k , (cd a , (cd b , (q , tt*)))))) go {k} (a ∨̇ b) c q = inr (inr (inr (inl (nn k , (cd a , (cd b , (q , tt*))))))) go {k} (a ⇒̇ b) c q = inr (inr (inr (inr (inl (nn k , (cd a , (cd b , (q , tt*)))))))) go {k} (¬̇ a) c q = inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , tt*)))))))) go {k} ⊤̇ c q = inr (inr (inr (inr (inr (inr (inl (nn k , (nn 0 , (q , sym (numeralL-fst 0)))))))))) go {k} ⊥̇ c q = inr (inr (inr (inr (inr (inr (inr (inl (nn k , (nn 0 , (q , sym (numeralL-fst 0))))))))))) go {k} (∃̇ a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , tt*))))))))))) go {k} (∀̇ a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , tt*)))))))))))) go {k} (∀̇∈ t a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (nn k , (ct t , (cd a , (q , tm1 t (cd a) c)))))))))))))) go {k} (∃̇∈ t a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (nn k , (ct t , (cd a , (q , tm1 t (cd a) c))))))))))))))