Bedrock可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。
交互式目录 · 依赖图固定宇宙层级 ℓ。保留这个层级参数，使构造可以在所需的各个大小处实例化，而不必把不同的宇宙视为同一个。
module L.Coding.CodeConstructibility {ℓ : Level} where
本章证明词项编码、公式编码与有穷环境图属于 L，再构造一棵可构造的树，汇集每个子公式上的数据并刻画其元素。
一个码是由配对数码造出的遗传有穷集，故它理应是 L 的元素，而本章就这么说。证明是沿公式构造子的一次归纳，里面什么也没有；但这条陈述使后续章节能把码当作模型的寻常元素，而非当作恰好躺在那里的层级集合。
它比看上去要紧。一个在 L 中内化的递归，其定义域取自 L 诸元素的小族，而此处那个族就是诸码；一个把码点名为常元的图，需要那个码是模型的元素，因为模型的对象语言没有别种常元。这两项要求都是这一条引理。
本章建立单个码的可构造性。可构造字母表上的全体码之集，由后面的 L.Coding.CodeSet 构造为 AllCodes，为可定义幂集的构造提供内部语法定义域。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
using ( ⁅_⁆s; ⁅_,_⁆; ⋃_; _∪_; module InfinitySet )
open InfinitySet using ( #_; sucV )
open hPropView 𝒮ʟ using ( S )
可构造的有序对与标签
prL 证明可构造性在编码配对下封闭，tagL 再把它特化为数码标签。这两条引理覆盖每个语法构造子的外层形状。
数码的可构造性同理，但这一结果早一章就已被用到，故其证明放在那一章。有序对可构造，因为模型有配对，而同一条等式又把它读回来；标签是左边放数码的对，故两者兼得。
两者都是同样的两步：先在模型内部把它构造出来，再沿「读出来就是那个东西」这条等式把它的成员关系搬过去。
prL : {a b : V ℓ} → ⟨ isL a ⟩ → ⟨ isL b ⟩ → ⟨ isL (pr a b) ⟩
prL {a} {b} pa pb =
subst (λ w → ⟨ isL w ⟩) (prʟ-fst (a , pa) (b , pb))
(prʟ (a , pa) (b , pb) .snd)
tagL : (k : ℕ) {x : V ℓ} → ⟨ isL x ⟩ → ⟨ isL (VCode.mkTag k x) ⟩
tagL k px = prL (numL k) px
对词项与公式编码的归纳
假设每个常元都指称一个可构造集合，codeTmL 与 codeL 通过结构归纳证明每个映射后的词项编码和公式编码都可构造。
先看词项。一个词项要么是变元，要么是常元，而两者正是词项所携带的两种标签：变元带它的索引数码，常元带它自己那个集合。因此，只要一个码所涉及的诸常元都可构造，这个码就可构造；本次归纳把这一点取作归纳假设，而不是假定根本没有常元。
这份一般性多花一条子句，换来的是对诸参数的处理。常元取自某层元素的公式，其编码与无参公式的编码一样是 L 的集合；正是这一点，使下面的递归得以遍历可构造层级实际由之造出的那些公式。无参情形是空类型处的实例。
然后是诸公式：十条子句，没有实质内容。每个构造子的码都是「子码之对」「单个子码」或「数码」三者之一的标签，而前面三个基础结果覆盖这三种形状。归纳沿无参公式而非它的嵌入进行，这一步不增加任何论证，因为嵌入是一次常元改名，按定义与每个构造子交换。
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where
codeTmL : ∀ {n} (t : Term K n) → ⟨ isL VCode.⌜ mapTm f t ⌝ᵗ ⟩
codeTmL (con c) = tagL 0 (h c)
codeTmL (var i) = tagL 1 (numL _)
codeL : ∀ {n} (φ : Formula K n) → ⟨ isL VCode.⌜ mapFo f φ ⌝ ⟩
codeL (t ∈̇ u) = tagL 0 (prL (codeTmL t) (codeTmL u))
codeL (t ≐ u) = tagL 1 (prL (codeTmL t) (codeTmL u))
codeL (φ ∧̇ ψ) = tagL 2 (prL (codeL φ) (codeL ψ))
codeL (φ ∨̇ ψ) = tagL 3 (prL (codeL φ) (codeL ψ))
codeL (φ ⇒̇ ψ) = tagL 4 (prL (codeL φ) (codeL ψ))
codeL ⊥̇ = tagL 5 (numL 0)
codeL (∃̇ φ) = tagL 6 (codeL φ)
codeL (∀̇ φ) = tagL 7 (codeL φ)
codeL (∀̇∈ t φ) = tagL 8 (prL (codeTmL t) (codeL φ))
codeL (∃̇∈ t φ) = tagL 9 (prL (codeTmL t) (codeL φ))
环境图的可构造性
envIsFinSet 把环境图等同于编码有序对的有穷集，envL 再用包含这些有序对的共同序数层把该图放入 L。
一个环境是一个有穷集：键是长度以下的诸数码，条目是诸对。事实上它恰恰就是那些对构成的有穷集，不差分毫，因为两者是同一个被抬升的索引类型的同一个像。说明这一点只需一行，而正是这一行使有穷族引理无须任何进一步论证便可施于环境。
由此，落在某层之上的环境立刻是 L 的元素：它的条目是「数码与该层的元素」之对，而两者在一步之后都落在该层里。不必沿长度递归，也不必用替换。
envIsFinSet : ∀ {n} (g : Fin n → V ℓ)
→ env g ≡ finSet n (λ i → pr (# (toℕ i)) (g i))
envIsFinSet g = refl
envL : (σ : V ℓ) (oσ : IsOrd σ) {n : ℕ} (g : Fin n → V ℓ)
→ ((i : Fin n) → ⟨ pr (# (toℕ i)) (g i) ∈ Lset σ ⟩)
→ ⟨ isL (env g) ⟩
envL σ oσ {n} g h =
subst (λ w → ⟨ isL w ⟩) (sym (envIsFinSet g))
(FinOf.finSetL σ oσ n (λ i → pr (# (toℕ i)) (g i)) h)
并与单点集
单点集与二元并构造既在层级的底层集合上实现，也在 L 的元素上实现；其引入与消去引理揭示相应成员关系。
再来两种形状，而模型直接供给两者。单点集是一物与自身之对，二元并是那个对之并，故两者都是模型自身的运算，沿底集读出。
每种形状都做两遍。一遍在底集上进行，配两条把单元集或二元并的元素读回来的引理；另一遍在模型自己的集合上进行，此时每一步都附带可构造性的证明，而同样那些引理经由「读出底集」那条等式重述一次。下面的递归在第二遍上进行，因此它造出的集合按构造就是 L 的元素，无须再作归纳。
sgl-out : (a x : V ℓ) → ⟨ x ∈ ⁅ a ⁆s ⟩ → x ≡ a
sgl-out a x h = rec₁ (setIsSet x a) (λ { (inl e) → e ; (inr e) → e })
(subst ⟨_⟩ (pair-spec a a x)
(subst (λ w → ⟨ x ∈ w ⟩) (sym (pair-singleton a)) h))
sgl-in : (a x : V ℓ) → x ≡ a → ⟨ x ∈ ⁅ a ⁆s ⟩
sgl-in a x e = subst (λ w → ⟨ x ∈ w ⟩) (pair-singleton a)
(subst ⟨_⟩ (sym (pair-spec a a x)) ∣ inl e ∣₁)
cup-out : (A B x : V ℓ) → ⟨ x ∈ (A ∪ B) ⟩ → ∥ (⟨ x ∈ A ⟩ ⊎ ⟨ x ∈ B ⟩) ∥₁
cup-out A B x h = rec₁ squash₁
(λ { (v , v∈ , x∈v) → map₁
(λ { (inl e) → inl (subst (λ w → ⟨ x ∈ w ⟩) e x∈v)
; (inr e) → inr (subst (λ w → ⟨ x ∈ w ⟩) e x∈v) })
(subst ⟨_⟩ (pair-spec A B v) v∈) })
(subst ⟨_⟩ (union-spec ⁅ A , B ⁆ x) h)
cup-inl : (A B x : V ℓ) → ⟨ x ∈ A ⟩ → ⟨ x ∈ (A ∪ B) ⟩
cup-inl A B x h = subst ⟨_⟩ (sym (union-spec ⁅ A , B ⁆ x))
∣ A , subst ⟨_⟩ (sym (pair-spec A B A)) ∣ inl refl ∣₁ , h ∣₁
cup-inr : (A B x : V ℓ) → ⟨ x ∈ B ⟩ → ⟨ x ∈ (A ∪ B) ⟩
cup-inr A B x h = subst ⟨_⟩ (sym (union-spec ⁅ A , B ⁆ x))
∣ B , subst ⟨_⟩ (sym (pair-spec A B B)) ∣ inr refl ∣₁ , h ∣₁
sglʟ : S → S
sglʟ a = pairʟ a a
sglʟ-fst : (a : S) → (sglʟ a) .fst ≡ ⁅ a .fst ⁆s
sglʟ-fst a = pairʟ-fst a a ∙ pair-singleton (a .fst)
cupʟ : S → S → S
cupʟ a b = unionʟ (pairʟ a b)
cupʟ-fst : (a b : S) → (cupʟ a b) .fst ≡ (a .fst ∪ b .fst)
cupʟ-fst a b = unionʟ-fst (pairʟ a b) ∙ cong (⋃_) (pairʟ-fst a b)
sglʟ-in : (a : S) (x : V ℓ) → x ≡ a .fst → ⟨ x ∈ (sglʟ a) .fst ⟩
sglʟ-in a x e = subst (λ w → ⟨ x ∈ w ⟩) (sym (sglʟ-fst a)) (sgl-in (a .fst) x e)
sglʟ-out : (a : S) (x : V ℓ) → ⟨ x ∈ (sglʟ a) .fst ⟩ → x ≡ a .fst
sglʟ-out a x h = sgl-out (a .fst) x (subst (λ w → ⟨ x ∈ w ⟩) (sglʟ-fst a) h)
cupʟ-inl : (a b : S) (x : V ℓ) → ⟨ x ∈ a .fst ⟩ → ⟨ x ∈ (cupʟ a b) .fst ⟩
cupʟ-inl a b x h = subst (λ w → ⟨ x ∈ w ⟩) (sym (cupʟ-fst a b))
(cup-inl (a .fst) (b .fst) x h)
cupʟ-inr : (a b : S) (x : V ℓ) → ⟨ x ∈ b .fst ⟩ → ⟨ x ∈ (cupʟ a b) .fst ⟩
cupʟ-inr a b x h = subst (λ w → ⟨ x ∈ w ⟩) (sym (cupʟ-fst a b))
(cup-inr (a .fst) (b .fst) x h)
cupʟ-out : (a b : S) (x : V ℓ) → ⟨ x ∈ (cupʟ a b) .fst ⟩
→ ∥ (⟨ x ∈ a .fst ⟩ ⊎ ⟨ x ∈ b .fst ⟩) ∥₁
cupʟ-out a b x h = cup-out (a .fst) (b .fst) x
(subst (λ w → ⟨ x ∈ w ⟩) (cupʟ-fst a b) h)
子公式递归
tree f φ 对 φ 的每个子公式 χ 合并其值 f χ；tree-inv 用贡献该元素的子公式描述任意元素，而 Parts 记录正向包含关系。
沿十个构造子作一次递归，收集什么由参数给出。它为每条子公式收集一样东西：给它键，得到下一节那个子公式闭包；给它条目，得到后续某章那张可满足性表。两者需要的是同一次求逆，故那次求逆在此只证一次，再实例化两次。
Of 说出这种集合的元素是什么：它是被收集之物之一，收集于某条子公式处，而那条子公式自己的集合包含于它所出自的那个集合之内。tree-inv 证明这一点，而 Parts 给出另一方向所需的诸成员关系，递归的每条子句所产生的每种形状各一条。
module _ {ℓ' : Level} {K : Type ℓ'} where
tree : (∀ {m} → Formula K m → S) → ∀ {n} → Formula K n → S
tree f φ@(t ∈̇ u) = sglʟ (f φ)
tree f φ@(t ≐ u) = sglʟ (f φ)
tree f φ@⊥̇ = sglʟ (f φ)
tree f φ@(a ∧̇ b) = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
tree f φ@(a ∨̇ b) = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
tree f φ@(a ⇒̇ b) = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
tree f φ@(∃̇ a) = cupʟ (sglʟ (f φ)) (tree f a)
tree f φ@(∀̇ a) = cupʟ (sglʟ (f φ)) (tree f a)
tree f φ@(∀̇∈ t a) = cupʟ (sglʟ (f φ)) (tree f a)
tree f φ@(∃̇∈ t a) = cupʟ (sglʟ (f φ)) (tree f a)
Of : (f g : ∀ {m} → Formula K m → S) {n : ℕ} → Formula K n → V ℓ
→ Type (ℓ-max (ℓ-suc ℓ) ℓ')
Of f g φ x = ∥ (Σ[ m ∶ ℕ ] Σ[ χ ∶ Formula K m ]
((x ≡ (f χ) .fst)
× ((z : V ℓ) → ⟨ z ∈ (tree g χ) .fst ⟩
→ ⟨ z ∈ (tree g φ) .fst ⟩))) ∥₁
private module _ (f g : ∀ {m} → Formula K m → S) where
one : ∀ {n} (φ : Formula K n) (x : V ℓ)
→ ⟨ x ∈ (sglʟ (f φ)) .fst ⟩ → Of f g φ x
one {n} φ x h = ∣ n , φ , sglʟ-out (f φ) x h , (λ _ hz → hz) ∣₁
wider : ∀ {n m} (φ : Formula K n) (χ : Formula K m) {x : V ℓ}
→ ((z : V ℓ) → ⟨ z ∈ (tree g χ) .fst ⟩ → ⟨ z ∈ (tree g φ) .fst ⟩)
→ Of f g χ x → Of f g φ x
wider _ _ s = map₁
(λ { (m , ψ , e , t) → m , ψ , e , (λ z hz → s z (t z hz)) })
un : ∀ {n m} (φ : Formula K n) (a : Formula K m)
→ ((z : V ℓ) → ⟨ z ∈ (cupʟ (sglʟ (g φ)) (tree g a)) .fst ⟩
→ ⟨ z ∈ (tree g φ) .fst ⟩)
→ ((x : V ℓ) → ⟨ x ∈ (tree f a) .fst ⟩ → Of f g a x)
→ (x : V ℓ) → ⟨ x ∈ (cupʟ (sglʟ (f φ)) (tree f a)) .fst ⟩ → Of f g φ x
un φ a into ra x h = rec₁ squash₁
(λ { (inl e) → one φ x e
; (inr e) → wider φ a
(λ z hz → into z (cupʟ-inr (sglʟ (g φ)) (tree g a) z hz))
(ra x e) })
(cupʟ-out (sglʟ (f φ)) (tree f a) x h)
bin : ∀ {n m} (φ : Formula K n) (a b : Formula K m)
→ ((z : V ℓ)
→ ⟨ z ∈ (cupʟ (sglʟ (g φ)) (cupʟ (tree g a) (tree g b))) .fst ⟩
→ ⟨ z ∈ (tree g φ) .fst ⟩)
→ ((x : V ℓ) → ⟨ x ∈ (tree f a) .fst ⟩ → Of f g a x)
→ ((x : V ℓ) → ⟨ x ∈ (tree f b) .fst ⟩ → Of f g b x)
→ (x : V ℓ)
→ ⟨ x ∈ (cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))) .fst ⟩
→ Of f g φ x
bin φ a b into ra rb x h = rec₁ squash₁
(λ { (inl e) → one φ x e
; (inr e) → rec₁ squash₁
(λ { (inl ea) → wider φ a (λ z hz → into z
(cupʟ-inr (sglʟ (g φ)) (cupʟ (tree g a) (tree g b)) z
(cupʟ-inl (tree g a) (tree g b) z hz)))
(ra x ea)
; (inr eb) → wider φ b (λ z hz → into z
(cupʟ-inr (sglʟ (g φ)) (cupʟ (tree g a) (tree g b)) z
(cupʟ-inr (tree g a) (tree g b) z hz)))
(rb x eb) })
(cupʟ-out (tree f a) (tree f b) x e) })
(cupʟ-out (sglʟ (f φ)) (cupʟ (tree f a) (tree f b)) x h)
module Parts (f : ∀ {m} → Formula K m → S) where
self : ∀ {n} (φ : Formula K n) → ⟨ (f φ) .fst ∈ (tree f φ) .fst ⟩
self φ@(t ∈̇ u) = sglʟ-in (f φ) _ refl
self φ@(t ≐ u) = sglʟ-in (f φ) _ refl
self φ@⊥̇ = sglʟ-in (f φ) _ refl
self φ@(a ∧̇ b) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
self φ@(a ∨̇ b) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
self φ@(a ⇒̇ b) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
self φ@(∃̇ a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
self φ@(∀̇ a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
self φ@(∀̇∈ t a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
self φ@(∃̇∈ t a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
left : ∀ {n m} (χ : Formula K n) (a b : Formula K m) (z : V ℓ)
→ ⟨ z ∈ (tree f a) .fst ⟩
→ ⟨ z ∈ (cupʟ (sglʟ (f χ)) (cupʟ (tree f a) (tree f b))) .fst ⟩
left χ a b z h = cupʟ-inr (sglʟ (f χ)) (cupʟ (tree f a) (tree f b)) z
(cupʟ-inl (tree f a) (tree f b) z h)
right : ∀ {n m} (χ : Formula K n) (a b : Formula K m) (z : V ℓ)
→ ⟨ z ∈ (tree f b) .fst ⟩
→ ⟨ z ∈ (cupʟ (sglʟ (f χ)) (cupʟ (tree f a) (tree f b))) .fst ⟩
right χ a b z h = cupʟ-inr (sglʟ (f χ)) (cupʟ (tree f a) (tree f b)) z
(cupʟ-inr (tree f a) (tree f b) z h)
only : ∀ {n m} (χ : Formula K n) (a : Formula K m) (z : V ℓ)
→ ⟨ z ∈ (tree f a) .fst ⟩
→ ⟨ z ∈ (cupʟ (sglʟ (f χ)) (tree f a)) .fst ⟩
only χ a z h = cupʟ-inr (sglʟ (f χ)) (tree f a) z h
tree-inv : (f g : ∀ {m} → Formula K m → S)
→ ∀ {n} (φ : Formula K n) (x : V ℓ)
→ ⟨ x ∈ (tree f φ) .fst ⟩ → Of f g φ x
tree-inv f g φ@(t ∈̇ u) = one f g φ
tree-inv f g φ@(t ≐ u) = one f g φ
tree-inv f g φ@⊥̇ = one f g φ
tree-inv f g φ@(a ∧̇ b) = bin f g φ a b (λ _ hz → hz)
(tree-inv f g a) (tree-inv f g b)
tree-inv f g φ@(a ∨̇ b) = bin f g φ a b (λ _ hz → hz)
(tree-inv f g a) (tree-inv f g b)
tree-inv f g φ@(a ⇒̇ b) = bin f g φ a b (λ _ hz → hz)
(tree-inv f g a) (tree-inv f g b)
tree-inv f g φ@(∃̇ a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)
tree-inv f g φ@(∀̇ a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)
tree-inv f g φ@(∀̇∈ t a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)
tree-inv f g φ@(∃̇∈ t a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)
子公式闭包
把通用树特化到公式键便得到 closure φ：这是一个可构造集合，包含 φ 的键及其所有子公式的键，并为每个构造子给出显式的元素映射。
对码的递归是相对某个槽陈述的：一个对直接子码封闭、且装着被问及的那个码的码集。最小的这种槽，就是一条公式自身诸子公式的码集，而它就是上面那个递归在键处的取值。
每个条目都携带元数，因为递归的键本身包含元数。因此，绑定子的子公式在后继元数处进入定义域。这是元数变化唯一显式出现的地方，因为各个框架正是按元数绑定相应数据。
可构造性无须另证：上面的递归在模型自身的集合上进行，证书随之一并给出。
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where
key : ∀ {n} → Formula K n → V ℓ
key {n} φ = pr (# n) VCode.⌜ mapFo f φ ⌝
keyL : ∀ {n} (φ : Formula K n) → ⟨ isL (key φ) ⟩
keyL φ = prL (numL _) (codeL f h φ)
private
keyS : ∀ {m} → Formula K m → S
keyS φ = key φ , keyL φ
closure : ∀ {n} → Formula K n → V ℓ
closure φ = (tree keyS φ) .fst
closureL : ∀ {n} (φ : Formula K n) → ⟨ isL (closure φ) ⟩
closureL φ = (tree keyS φ) .snd
小结
这些结果把语法编码、环境及按子公式索引的汇集都放进 L；余下引理把闭包元素还原为具体的子公式键，供后面的有界递归使用。
codeL 说每个码都是 L 的元素，而 numL、prL 与 tagL 是它所由构造的三种形状。有了它，一个码就可以被点名为模型对象语言的常元，而一族码就可以充当某个已内化递归的定义域。
envL 随后把一个环境放进 L，既不沿长度递归，也不用替换，因为一个环境恰恰就是它的诸条目构成的有穷集。closure 是「对一个码的递归」所能相对陈述的最小的槽，而 closureL 把它的证书从造出它的那个递归上读下来，不必再证第二次。
全体码之集仍然不是 L 的元素，也仍然不需要是。
把闭包读回来
closure-inv 应用通用的树反演，证明 closure φ 的每个元素都是某个子公式的键，且该子公式的闭包嵌入 φ 的闭包。
对码进行递归时，必须具体知道定义域中的元素来自哪些公式。下面的引理给出所需刻画：闭包的每个元素都是某条公式的键，并且该公式自身的闭包包含在原公式的闭包中。后一个包含关系正是归纳所需的条件，它保证归纳假设在处理相应子公式时可用。
这条结论与「键属于自身闭包」都直接来自上面递归在键处的两条读式，因此这里都不需要新的归纳。
Inv : ∀ {n} → Formula K n → V ℓ → Type (ℓ-suc ℓ)
Inv φ x = Of keyS keyS φ x
closure-inv : ∀ {n} (φ : Formula K n) (x : V ℓ)
→ ⟨ x ∈ closure φ ⟩ → Inv φ x
closure-inv φ x hx = tree-inv keyS keyS φ x hx
key∈closure : ∀ {n} (φ : Formula K n) → ⟨ key φ ∈ closure φ ⟩
key∈closure φ = Parts.self keyS φ
从公式键恢复公式
已知某集合等于一个公式键时，最后的引理把该见证转化为一个显式公式，并保留其闭包到原闭包的包含关系。
封闭性谓词提的要求以构造子标签为索引，而它所谈论的公式以构造子为索引。把这两者对上，是第一个实例里唯一真正的活；而逐条去做会是十条公式乘七项要求。不必如此，因为那项要求可以从标签算出来：一个以标签为索引的类型族、一个以公式为索引的函数，而键的单射性所给出的那条标签等式把后者搬到前者上。
在标签之下，一个键是元数与码之对，这两层都由配对的单射性确定。由此得出：保持元数的构造子在所读出的元数处要求其诸分量，抬升元数的在后继处要求分量，而没有子公式的构造子则不要求任何分量。
module _ (C : V ℓ) where
BothSame : V ℓ → V ℓ → Type (ℓ-suc ℓ)
BothSame ar p = (u v : V ℓ) → p ≡ pr u v
→ ⟨ pr ar u ∈ C ⟩ × ⟨ pr ar v ∈ C ⟩
SecondSucc : V ℓ → V ℓ → Type (ℓ-suc ℓ)
SecondSucc ar p = (u v : V ℓ) → p ≡ pr u v → ⟨ pr (sucV ar) v ∈ C ⟩
Concl : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
Concl 2 ar p = BothSame ar p
Concl 3 ar p = BothSame ar p
Concl 4 ar p = BothSame ar p
Concl 6 ar p = ⟨ pr (sucV ar) p ∈ C ⟩
Concl 7 ar p = ⟨ pr (sucV ar) p ∈ C ⟩
Concl 8 ar p = SecondSucc ar p
Concl 9 ar p = SecondSucc ar p
Concl _ _ _ = ⊤*
private
Below : ∀ {n} → Formula K n → Type (ℓ-suc ℓ)
Below φ = (z : V ℓ) → ⟨ z ∈ closure φ ⟩ → ⟨ z ∈ C ⟩
inC : ∀ {n m} (φ : Formula K n) (a : Formula K m)
→ Below φ → ⟨ key a ∈ closure φ ⟩ → {w : V ℓ} → key a ≡ w → ⟨ w ∈ C ⟩
inC φ a below mem q = subst (λ w → ⟨ w ∈ C ⟩) q (below (key a) mem)
atTag : ∀ {m k : ℕ} {ar p : V ℓ} (j : ℕ) (q : V ℓ)
→ pr (# m) (VCode.mkTag j q) ≡ pr ar (pr (# k) p)
→ (j ≡ k) × ((# m ≡ ar) × (q ≡ p))
atTag j q e = VCode.mkTag-inj (pr-inj e .snd) .fst
, (pr-inj e .fst , VCode.mkTag-inj (pr-inj e .snd) .snd)
bothOf : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
→ Below φ' → ⟨ key a ∈ closure φ' ⟩ → ⟨ key b ∈ closure φ' ⟩
→ (ar p : V ℓ) → # m' ≡ ar
→ pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝ ≡ p
→ BothSame ar p
bothOf φ' a b below ma mb ar p qa qp u v qu =
inC φ' a below ma (cong₂ pr qa (pr-inj (qp ∙ qu) .fst))
, inC φ' b below mb (cong₂ pr qa (pr-inj (qp ∙ qu) .snd))
oneOf : ∀ {n m'} (φ' : Formula K n) (a : Formula K m')
→ Below φ' → ⟨ key a ∈ closure φ' ⟩
→ (ar p : V ℓ) → # m' ≡ ar → VCode.⌜ mapFo f a ⌝ ≡ p
→ ⟨ pr ar p ∈ C ⟩
oneOf φ' a below ma ar p qa qp = inC φ' a below ma (cong₂ pr qa qp)
upOf : ∀ {n m'} (φ' : Formula K n) (a : Formula K (suc m'))
→ Below φ' → ⟨ key a ∈ closure φ' ⟩
→ (ar p : V ℓ) → # m' ≡ ar → VCode.⌜ mapFo f a ⌝ ≡ p
→ ⟨ pr (sucV ar) p ∈ C ⟩
upOf φ' a below ma ar p qa qp =
inC φ' a below ma (cong₂ pr (cong sucV qa) qp)
sndUpOf : ∀ {n m'} (φ' : Formula K n) (t : Term K m')
(a : Formula K (suc m'))
→ Below φ' → ⟨ key a ∈ closure φ' ⟩
→ (ar p : V ℓ) → # m' ≡ ar
→ pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝ ≡ p
→ SecondSucc ar p
sndUpOf φ' t a below ma ar p qa qp u v qu =
inC φ' a below ma (cong₂ pr (cong sucV qa) (pr-inj (qp ∙ qu) .snd))
left : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
→ ⟨ key a ∈ (cupʟ (sglʟ (keyS φ'))
(cupʟ (tree keyS a) (tree keyS b))) .fst ⟩
left φ' a b = Parts.left keyS φ' a b (key a) (key∈closure a)
right : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
→ ⟨ key b ∈ (cupʟ (sglʟ (keyS φ'))
(cupʟ (tree keyS a) (tree keyS b))) .fst ⟩
right φ' a b = Parts.right keyS φ' a b (key b) (key∈closure b)
only : ∀ {n m'} (φ' : Formula K n) (a : Formula K m')
→ ⟨ key a ∈ (cupʟ (sglʟ (keyS φ')) (tree keyS a)) .fst ⟩
only φ' a = Parts.only keyS φ' a (key a) (key∈closure a)
byTag : ∀ {m} (φ : Formula K m) (k : ℕ) (ar p : V ℓ)
→ Below φ → key φ ≡ pr ar (pr (# k) p) → Concl k ar p
byTag (t ∈̇ u) k ar p below eq = subst (λ j → Concl j ar p)
(atTag 0 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ) eq .fst) tt*
byTag (t ≐ u) k ar p below eq = subst (λ j → Concl j ar p)
(atTag 1 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ) eq .fst) tt*
byTag ⊥̇ k ar p below eq = subst (λ j → Concl j ar p)
(atTag 5 (# 0) eq .fst) tt*
byTag φ@(a ∧̇ b) k ar p below eq =
let r = atTag 2 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
subst (λ j → Concl j ar p) (r .fst)
(bothOf φ a b below (left φ a b) (right φ a b) ar p
(r .snd .fst) (r .snd .snd))
byTag φ@(a ∨̇ b) k ar p below eq =
let r = atTag 3 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
subst (λ j → Concl j ar p) (r .fst)
(bothOf φ a b below (left φ a b) (right φ a b) ar p
(r .snd .fst) (r .snd .snd))
byTag φ@(a ⇒̇ b) k ar p below eq =
let r = atTag 4 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
subst (λ j → Concl j ar p) (r .fst)
(bothOf φ a b below (left φ a b) (right φ a b) ar p
(r .snd .fst) (r .snd .snd))
byTag φ@(∃̇ a) k ar p below eq =
let r = atTag 6 VCode.⌜ mapFo f a ⌝ eq in
subst (λ j → Concl j ar p) (r .fst)
(upOf φ a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
byTag φ@(∀̇ a) k ar p below eq =
let r = atTag 7 VCode.⌜ mapFo f a ⌝ eq in
subst (λ j → Concl j ar p) (r .fst)
(upOf φ a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
byTag φ@(∀̇∈ t a) k ar p below eq =
let r = atTag 8 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝) eq in
subst (λ j → Concl j ar p) (r .fst)
(sndUpOf φ t a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
byTag φ@(∃̇∈ t a) k ar p below eq =
let r = atTag 9 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝) eq in
subst (λ j → Concl j ar p) (r .fst)
(sndUpOf φ t a below (only φ a) ar p (r .snd .fst) (r .snd .snd))