BedrockA good table has only one value
唯一性那一半。一张在子码封闭的索引集上满足十二条子句、且在其中每个键处都作答的表，在每个键处记录的就是元语言递归在那里造出的取值，别无其他。正是这一点使那个图单值。
它是对着那个典范取值陈述的，不是在两张任意的表之间。两种形式是同一次归纳，而钉住一侧的那种更短，也是递归所消费的那种：funct 需要的是「某索引处的取值被决定」，而被决定的取值来自元语言的递归。
这条陈述的形状不是口味问题。索引与取值都是变元，而那个键经一条等式抵达，与每条子句读式的写法完全一致；把某一情形陈述在「键已经代入」的形式上，就等于把两个具体的集合构造塞进一个满足关系里，而那在任何合理时间内都不会通过类型检查。本章在它的第一个情形上学到了这一点。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.Unique {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( closedAt; domAt; domAt-in; botClauseAt; botClause-out; topClauseAt ; topClause-out; andClauseAt; orClauseAt; propClause-out ; interAt; unionAt; yc7; ya7; yb7; negClauseAt; negClause-out ; unSameClosed-out; impClauseAt; impClause-out ; memClauseAt; eqClauseAt; memRel; eqRel; atomClause-out ; atomBody; atomBody-in; atomBody-out ; extAt-out; extAt-in; existClauseAt; quantClause-out; body∃ ; body∃-in; body∃-out; forallClauseAt; body∀; body∀-in; body∀-out ; unSuccClosed-out; consAtL-transport; allInClauseAt; bndClause-out ; bodyAll; bodyAll-in; bodyAll-out; exInClauseAt ; bodyEx; bodyEx-in; bodyEx-out; binSuccClosed-out ; binSameClosed-out; prʟ-fst; module LCode; numL ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Coding.Sat {ℓ} lem using ( Sat; Sat-mem; cond∈-in; cond∈-out; cond≐-in; cond≐-out ; cond∃-in; cond∃-out; cond∀-in; cond∀-out ; cond∀∈-in; cond∀∈-out; cond∃∈-in; cond∃∈-out ) open import L.Coding.Table {ℓ} lem using ( keyʟ; keyʟ-shape-in ) open import L.Coding.EnvSet {ℓ} lem using ( envSet ) open import L.Coding.Sound {ℓ} lem using ( module AmbientHolds; module Ambient; termAgree ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ ) open import Cubical.Data.Sum using ( inl; inr ) open import Cubical.Data.Unit using ( tt* ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫↪ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; sucV ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) private nn : ℕ → S nn k = # k , numL k
什么叫一张好表
三件，按那个图将要陈述它们的次序：索引集含有其成员的诸子码、表在每个索引处作答、以及十二条子句成立。前两件是存在性那一半必须造出来的东西；此处它们是假设，因为那张表如今是任意的。
module Good {k : ℕ} (γ : S ^ k) (Ci Ti Bi : Fin k) where private B C T : S B = lookup Bi γ C = lookup Ci γ T = lookup Ti γ Closed : Type (ℓ-suc ℓ) Closed = ⟨ γ ⊨ closedAt Ci ⟩ Total : Type (ℓ-suc ℓ) Total = ⟨ γ ⊨ domAt Ti Ci ⟩ Bot : Type (ℓ-suc ℓ) Bot = ⟨ γ ⊨ botClauseAt Ci Ti ⟩ Top : Type (ℓ-suc ℓ) Top = ⟨ γ ⊨ topClauseAt Ci Ti Bi ⟩ And : Type (ℓ-suc ℓ) And = ⟨ γ ⊨ andClauseAt Ci Ti ⟩ Or : Type (ℓ-suc ℓ) Or = ⟨ γ ⊨ orClauseAt Ci Ti ⟩ Neg : Type (ℓ-suc ℓ) Neg = ⟨ γ ⊨ negClauseAt Ci Ti Bi ⟩ Imp : Type (ℓ-suc ℓ) Imp = ⟨ γ ⊨ impClauseAt Ci Ti Bi ⟩ Mem : Type (ℓ-suc ℓ) Mem = ⟨ γ ⊨ memClauseAt Ci Ti Bi ⟩ Eq : Type (ℓ-suc ℓ) Eq = ⟨ γ ⊨ eqClauseAt Ci Ti Bi ⟩ Ex : Type (ℓ-suc ℓ) Ex = ⟨ γ ⊨ existClauseAt Ci Ti Bi ⟩ All : Type (ℓ-suc ℓ) All = ⟨ γ ⊨ forallClauseAt Ci Ti Bi ⟩ AllIn : Type (ℓ-suc ℓ) AllIn = ⟨ γ ⊨ allInClauseAt Ci Ti Bi ⟩ ExIn : Type (ℓ-suc ℓ) ExIn = ⟨ γ ⊨ exInClauseAt Ci Ti Bi ⟩ ai0 : ∀ {j} → Fin (suc j) ai0 = zero ai1 : ∀ {j} → Fin (suc (suc j)) ai1 = suc zero ai2 : ∀ {j} → Fin (suc (suc (suc j))) ai2 = suc (suc zero) ai5 : ∀ {j} → Fin (suc (suc (suc (suc (suc (suc j)))))) ai5 = suc (suc (suc (suc (suc zero)))) ai6 : ∀ {j} → Fin (suc (suc (suc (suc (suc (suc (suc j))))))) ai6 = suc (suc (suc (suc (suc (suc zero))))) toS : (v : S) (w : V ℓ) → ⟨ w ∈ fst v ⟩ → S toS v w hw = w , isL-trans hw (snd v) kkey : ∀ {j} (χ : Formula S j) → pr (# j) (fst LCode.⌜ χ ⌝) ≡ fst (keyʟ χ) kkey {j} χ = cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst j)) ∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝) kkeyS : ∀ {j} (χ : Formula S (suc j)) → pr (sucV (# j)) (fst LCode.⌜ χ ⌝) ≡ fst (keyʟ χ) kkeyS {j} χ = cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst (suc j))) ∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝) upS : ∀ {j} (χ : Formula S (suc j)) (v : S) → ⟨ pr (fst (keyʟ χ)) (fst v) ∈ fst T ⟩ → ⟨ pr (pr (sucV (# j)) (fst LCode.⌜ χ ⌝)) (fst v) ∈ fst T ⟩ upS χ v h = subst (λ w → ⟨ pr w (fst v) ∈ fst T ⟩) (sym (kkeyS χ)) h up : ∀ {j} (χ : Formula S j) (v : S) → ⟨ pr (fst (keyʟ χ)) (fst v) ∈ fst T ⟩ → ⟨ pr (pr (# j) (fst LCode.⌜ χ ⌝)) (fst v) ∈ fst T ⟩ up χ v h = subst (λ w → ⟨ pr w (fst v) ∈ fst T ⟩) (sym (kkey χ)) h Pinned : ∀ {m} → Formula S m → Type (ℓ-suc ℓ) Pinned {m} ψ = (c y : S) → fst c ≡ fst (keyʟ ψ) → ⟨ fst c ∈ fst C ⟩ → ⟨ pr (fst c) (fst y) ∈ fst T ⟩ → fst y ≡ fst (Sat B ψ)
自己钉住自己的那个常量
第一种情形，也是什么都不需要的那一种：⊥̇ 的子句说那个取值为空，而递归当初是用「没有东西满足的条件」从周遭集合把它的取值雕出来的，而两个空集相等。不必递周遭集合进去，没有子取值要替换，也用不上归纳假设。
bot : Bot → ∀ {m} → Pinned (⊥̇ {n = m}) bot hbot {m} c y q c∈ hy = extensionalV (λ w → ⇔toPath (λ hw → Empty.rec* (empty (w , isL-trans hw (snd y)) hw)) (λ hw → Empty.rec* (subst ⟨_⟩ (Sat-mem B (⊥̇ {n = m}) (w , isL-trans hw (snd (Sat B (⊥̇ {n = m}))))) hw .snd))) where empty = botClause-out Ci Ti γ hbot c (nn m) (numeralL 0) y c∈ (q ∙ keyʟ-shape-in (⊥̇ {n = m})) hy .fst
由周遭集合钉住的那个常量
第二个常量，也是第一条必须递出一个周遭集合、而非消费一个的情形。子句说那个取值就是诸环境之集；递归当初用「一切都满足的条件」从那个集合把它的取值雕出来，故那个取值又是那个集合。递出只是把那份一致性施用一次，而诸元数与载体由 refl 对上，因为框架把它们放在子句所看之处。
top : Top → ∀ {m} → Pinned (⊤̇ {n = m}) top htop {m} c y q c∈ hy = extensionalV (λ w → ⇔toPath (λ hw → subst ⟨_⟩ (sym (Sat-mem B (⊤̇ {n = m}) (sw w hw))) (e .fst (sw w hw) hw , tt*)) (λ hw → e .snd (sw' w hw) (subst ⟨_⟩ (Sat-mem B (⊤̇ {n = m}) (sw' w hw)) hw .fst))) where δ' = envSet B m ∷ y ∷ numeralL 0 ∷ nn m ∷ c ∷ γ hE = AmbientHolds.holds B δ' zero (suc (suc (suc zero))) (suc (suc (suc (suc (suc Bi))))) m refl refl refl e = topClause-out Ci Ti Bi γ htop c (nn m) (numeralL 0) y (envSet B m) c∈ (q ∙ keyʟ-shape-in (⊤̇ {n = m})) hy hE sw : (w : V ℓ) → ⟨ w ∈ fst y ⟩ → S sw w hw = w , isL-trans hw (snd y) sw' : (w : V ℓ) → ⟨ w ∈ fst (Sat B (⊤̇ {n = m})) ⟩ → S sw' w hw = w , isL-trans hw (snd (Sat B (⊤̇ {n = m})))
第一条用上归纳假设的情形
合取，以及随之而来、余下十条都要走的那个形状。封闭性把诸子键放进索引，全性使表在每个子键处都有条目，归纳假设说那些条目就是递归的诸取值，子句说键处的取值是它们的交，而递归当初正是用同一个条件把它的取值雕出来的。那些条目是仅仅到手的，而这不花分文，因为目标是一条集合之间的等式。
and : Closed → Total → And → ∀ {m} (a' b' : Formula S m) → Pinned a' → Pinned b' → Pinned (a' ∧̇ b') and hcl hdom hand {m} a' b' ia ib c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (a' ∧̇ b')))) (λ { (ya , hya) → PT.rec (setIsSet (fst y) (fst (Sat B (a' ∧̇ b')))) (λ { (yb , hyb) → let ea = ia (keyʟ a') ya refl (ka .fst) hya eb = ib (keyʟ b') yb refl (ka .snd) hyb e = propClause-out Ci Ti 2 (interAt yc7 ya7 yb7) γ hand c (nn m) ca cb y ya yb c∈ shape hy (up a' ya hya) (up b' yb hyb) in extensionalV (λ w → ⇔toPath (λ hw → subst ⟨_⟩ (sym (Sat-mem B (a' ∧̇ b') (toS y w hw))) ( subst ⟨_⟩ (Sat-mem B a' (toS y w hw)) (subst (λ v → ⟨ w ∈ v ⟩) ea (e .fst (toS y w hw) hw .fst)) .fst , ( subst (λ v → ⟨ w ∈ v ⟩) ea (e .fst (toS y w hw) hw .fst) , subst (λ v → ⟨ w ∈ v ⟩) eb (e .fst (toS y w hw) hw .snd) ) )) (λ hw → let r = subst ⟨_⟩ (Sat-mem B (a' ∧̇ b') (toS (Sat B _) w hw)) hw in e .snd (toS (Sat B _) w hw) ( subst (λ v → ⟨ w ∈ v ⟩) (sym ea) (r .snd .fst) , subst (λ v → ⟨ w ∈ v ⟩) (sym eb) (r .snd .snd) ))) }) (domAt-in Ti Ci γ hdom (keyʟ b') (ka .snd)) }) (domAt-in Ti Ci γ hdom (keyʟ a') (ka .fst)) where ca cb : S ca = LCode.⌜ a' ⌝ cb = LCode.⌜ b' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 2) (pr (fst ca) (fst cb))) shape = q ∙ keyʟ-shape-in (a' ∧̇ b') ∙ cong (λ w → pr (# m) (pr (# 2) w)) (prʟ-fst ca cb) ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ × ⟨ fst (keyʟ b') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkey a') (r .fst) , subst (λ w → ⟨ w ∈ fst C ⟩) (kkey b') (r .snd) where r = binSameClosed-out Ci 2 γ (hcl .fst) c (nn m) ca cb c∈ shape or : Closed → Total → Or → ∀ {m} (a' b' : Formula S m) → Pinned a' → Pinned b' → Pinned (a' ∨̇ b') or hcl hdom hor {m} a' b' ia ib c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (a' ∨̇ b')))) (λ { (ya , hya) → PT.rec (setIsSet (fst y) (fst (Sat B (a' ∨̇ b')))) (λ { (yb , hyb) → let ea = ia (keyʟ a') ya refl (ka .fst) hya eb = ib (keyʟ b') yb refl (ka .snd) hyb e = propClause-out Ci Ti 3 (unionAt yc7 ya7 yb7) γ hor c (nn m) ca cb y ya yb c∈ shape hy (up a' ya hya) (up b' yb hyb) in extensionalV (λ w → ⇔toPath (λ hw → PT.rec (snd (w ∈ fst (Sat B (a' ∨̇ b')))) (λ { (inl h) → subst ⟨_⟩ (sym (Sat-mem B (a' ∨̇ b') (toS y w hw))) ( subst ⟨_⟩ (Sat-mem B a' (toS y w hw)) (subst (λ v → ⟨ w ∈ v ⟩) ea h) .fst , ∣ inl (subst (λ v → ⟨ w ∈ v ⟩) ea h) ∣₁ ) ; (inr h) → subst ⟨_⟩ (sym (Sat-mem B (a' ∨̇ b') (toS y w hw))) ( subst ⟨_⟩ (Sat-mem B b' (toS y w hw)) (subst (λ v → ⟨ w ∈ v ⟩) eb h) .fst , ∣ inr (subst (λ v → ⟨ w ∈ v ⟩) eb h) ∣₁ ) }) (e .fst (toS y w hw) hw)) (λ hw → e .snd (toS (Sat B _) w hw) (PT.map (λ { (inl h) → inl (subst (λ v → ⟨ w ∈ v ⟩) (sym ea) h) ; (inr h) → inr (subst (λ v → ⟨ w ∈ v ⟩) (sym eb) h) }) (subst ⟨_⟩ (Sat-mem B (a' ∨̇ b') (toS (Sat B _) w hw)) hw .snd)))) }) (domAt-in Ti Ci γ hdom (keyʟ b') (ka .snd)) }) (domAt-in Ti Ci γ hdom (keyʟ a') (ka .fst)) where ca cb : S ca = LCode.⌜ a' ⌝ cb = LCode.⌜ b' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 3) (pr (fst ca) (fst cb))) shape = q ∙ keyʟ-shape-in (a' ∨̇ b') ∙ cong (λ w → pr (# m) (pr (# 3) w)) (prʟ-fst ca cb) ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ × ⟨ fst (keyʟ b') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkey a') (r .fst) , subst (λ w → ⟨ w ∈ fst C ⟩) (kkey b') (r .snd) where r = binSameClosed-out Ci 3 γ (hcl .snd .fst) c (nn m) ca cb c∈ shape
否定，最后一种新组合
三样成分一次到齐：一个要递出的周遭集合、一个要认同的子取值、一条要用的归纳假设。余下每一种情形都是这三样加一条不同的子句，没有谁需要第四样成分。
neg : Closed → Total → Neg → ∀ {m} (a' : Formula S m) → Pinned a' → Pinned (¬̇ a') neg hcl hdom hneg {m} a' ia c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (¬̇ a')))) (λ { (ya , hya) → let ea = ia (keyʟ a') ya refl ka hya δ' = envSet B m ∷ ya ∷ y ∷ ca ∷ nn m ∷ c ∷ γ hE = AmbientHolds.holds B δ' zero (suc (suc (suc (suc zero)))) (suc (suc (suc (suc (suc (suc Bi)))))) m refl refl refl e = negClause-out Ci Ti Bi γ hneg c (nn m) ca y ya (envSet B m) c∈ shape hy (up a' ya hya) hE in extensionalV (λ w → ⇔toPath (λ hw → subst ⟨_⟩ (sym (Sat-mem B (¬̇ a') (toS y w hw))) ( e .fst (toS y w hw) hw .fst , (λ h → e .fst (toS y w hw) hw .snd (subst (λ v → ⟨ w ∈ v ⟩) (sym ea) h)) )) (λ hw → let r = subst ⟨_⟩ (Sat-mem B (¬̇ a') (toS (Sat B (¬̇ a')) w hw)) hw in e .snd (toS (Sat B (¬̇ a')) w hw) ( r .fst , (λ h → r .snd (subst (λ v → ⟨ w ∈ v ⟩) ea h)) ))) }) (domAt-in Ti Ci γ hdom (keyʟ a') ka) where ca : S ca = LCode.⌜ a' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 5) (fst ca)) shape = q ∙ keyʟ-shape-in (¬̇ a') ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkey a') (unSameClosed-out Ci 5 γ (hcl .snd .snd .snd .fst) c (nn m) ca c∈ shape)
蕴含
两个子取值加一个周遭集合，即否定与合取合在一处。两侧的等式都是对象语言自己的箭头，而那是写下诸子句的那一章所作、也不得不作的选择：合并的写法要用排中律，而两章都不取它。
imp : Closed → Total → Imp → ∀ {m} (a' b' : Formula S m) → Pinned a' → Pinned b' → Pinned (a' ⇒̇ b') imp hcl hdom himp {m} a' b' ia ib c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (a' ⇒̇ b')))) (λ { (ya , hya) → PT.rec (setIsSet (fst y) (fst (Sat B (a' ⇒̇ b')))) (λ { (yb , hyb) → let ea = ia (keyʟ a') ya refl (ka .fst) hya eb = ib (keyʟ b') yb refl (ka .snd) hyb δ' = envSet B m ∷ yb ∷ ya ∷ y ∷ cb ∷ ca ∷ nn m ∷ c ∷ γ hE = AmbientHolds.holds B δ' zero (suc (suc (suc (suc (suc (suc zero)))))) (suc (suc (suc (suc (suc (suc (suc (suc Bi)))))))) m refl refl refl e = impClause-out Ci Ti Bi γ himp c (nn m) ca cb y ya yb (envSet B m) c∈ shape hy (up a' ya hya) (up b' yb hyb) hE in extensionalV (λ w → ⇔toPath (λ hw → subst ⟨_⟩ (sym (Sat-mem B (a' ⇒̇ b') (toS y w hw))) ( e .fst (toS y w hw) hw .fst , (λ h → subst (λ v → ⟨ w ∈ v ⟩) eb (e .fst (toS y w hw) hw .snd (subst (λ v → ⟨ w ∈ v ⟩) (sym ea) h))) )) (λ hw → let r = subst ⟨_⟩ (Sat-mem B (a' ⇒̇ b') (toS (Sat B (a' ⇒̇ b')) w hw)) hw in e .snd (toS (Sat B (a' ⇒̇ b')) w hw) ( r .fst , (λ h → subst (λ v → ⟨ w ∈ v ⟩) (sym eb) (r .snd (subst (λ v → ⟨ w ∈ v ⟩) ea h))) ))) }) (domAt-in Ti Ci γ hdom (keyʟ b') (ka .snd)) }) (domAt-in Ti Ci γ hdom (keyʟ a') (ka .fst)) where ca cb : S ca = LCode.⌜ a' ⌝ cb = LCode.⌜ b' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 4) (pr (fst ca) (fst cb))) shape = q ∙ keyʟ-shape-in (a' ⇒̇ b') ∙ cong (λ w → pr (# m) (pr (# 4) w)) (prʟ-fst ca cb) ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ × ⟨ fst (keyʟ b') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkey a') (r .fst) , subst (λ w → ⟨ w ∈ fst C ⟩) (kkey b') (r .snd) where r = binSameClosed-out Ci 4 γ (hcl .snd .snd .fst) c (nn m) ca cb c∈ shape
两个原子
一个原子没有子公式，故它既不要封闭性、也不要归纳假设：递出一个周遭集合，再把词项桥用两次。子句从两个码读出那两个取值，递归从两个词项读出它们，而那座桥说它们一致。
mem : Mem → ∀ {m} (t u : Term S m) → Pinned (t ∈̇ u) mem hmem {m} t u c y q c∈ hy = extensionalV (λ w → ⇔toPath (λ hw → let sy = toS y w hw ab = atomBody-out memRel (sy ∷ δ') (extAt-out (suc zero) (atomBody memRel) δ' e sy hw) in subst ⟨_⟩ (sym (Sat-mem B (t ∈̇ u) sy)) ( ab .fst , cond∈-in B t u sy (PT.map (λ { (v , (x , (ht , (hu , hr)))) → v , x , ( termAgree t (x ∷ v ∷ sy ∷ δ') ai6 ai2 ai1 (x ∷ v ∷ sy ∷ []) ai1 ai2 refl refl refl .fst ht , ( termAgree u (x ∷ v ∷ sy ∷ δ') ai5 ai2 ai0 (x ∷ v ∷ sy ∷ []) ai0 ai2 refl refl refl .fst hu , hr ) ) }) (ab .snd)) )) (λ hw → let sw = toS (Sat B (t ∈̇ u)) w hw h = subst ⟨_⟩ (Sat-mem B (t ∈̇ u) sw) hw in extAt-in (suc zero) (atomBody memRel) δ' e sw (atomBody-in memRel (sw ∷ δ') (h .fst) (PT.map (λ { (v , (x , (ht , (hu , hr)))) → v , x , ( termAgree t (x ∷ v ∷ sw ∷ δ') ai6 ai2 ai1 (x ∷ v ∷ sw ∷ []) ai1 ai2 refl refl refl .snd ht , ( termAgree u (x ∷ v ∷ sw ∷ δ') ai5 ai2 ai0 (x ∷ v ∷ sw ∷ []) ai0 ai2 refl refl refl .snd hu , hr ) ) }) (cond∈-out B t u sw (h .snd)))))) where ct cu : S ct = LCode.⌜ t ⌝ᵗ cu = LCode.⌜ u ⌝ᵗ δ' = envSet B m ∷ y ∷ cu ∷ ct ∷ nn m ∷ c ∷ γ shape : fst c ≡ pr (fst (nn m)) (pr (# 0) (pr (fst ct) (fst cu))) shape = q ∙ keyʟ-shape-in (t ∈̇ u) ∙ cong (λ w → pr (# m) (pr (# 0) w)) (prʟ-fst ct cu) hE = AmbientHolds.holds B δ' zero (suc (suc (suc (suc zero)))) (suc (suc (suc (suc (suc (suc Bi)))))) m refl refl refl e = atomClause-out Ci Ti Bi 0 memRel γ hmem c (nn m) ct cu y (envSet B m) c∈ shape hy hE eq : Eq → ∀ {m} (t u : Term S m) → Pinned (t ≐ u) eq heq {m} t u c y q c∈ hy = extensionalV (λ w → ⇔toPath (λ hw → let sy = toS y w hw ab = atomBody-out eqRel (sy ∷ δ') (extAt-out (suc zero) (atomBody eqRel) δ' e sy hw) in subst ⟨_⟩ (sym (Sat-mem B (t ≐ u) sy)) ( ab .fst , cond≐-in B t u sy (PT.map (λ { (v , (x , (ht , (hu , hr)))) → v , x , ( termAgree t (x ∷ v ∷ sy ∷ δ') ai6 ai2 ai1 (x ∷ v ∷ sy ∷ []) ai1 ai2 refl refl refl .fst ht , ( termAgree u (x ∷ v ∷ sy ∷ δ') ai5 ai2 ai0 (x ∷ v ∷ sy ∷ []) ai0 ai2 refl refl refl .fst hu , hr ) ) }) (ab .snd)) )) (λ hw → let sw = toS (Sat B (t ≐ u)) w hw h = subst ⟨_⟩ (Sat-mem B (t ≐ u) sw) hw in extAt-in (suc zero) (atomBody eqRel) δ' e sw (atomBody-in eqRel (sw ∷ δ') (h .fst) (PT.map (λ { (v , (x , (ht , (hu , hr)))) → v , x , ( termAgree t (x ∷ v ∷ sw ∷ δ') ai6 ai2 ai1 (x ∷ v ∷ sw ∷ []) ai1 ai2 refl refl refl .snd ht , ( termAgree u (x ∷ v ∷ sw ∷ δ') ai5 ai2 ai0 (x ∷ v ∷ sw ∷ []) ai0 ai2 refl refl refl .snd hu , hr ) ) }) (cond≐-out B t u sw (h .snd)))))) where ct cu : S ct = LCode.⌜ t ⌝ᵗ cu = LCode.⌜ u ⌝ᵗ δ' = envSet B m ∷ y ∷ cu ∷ ct ∷ nn m ∷ c ∷ γ shape : fst c ≡ pr (fst (nn m)) (pr (# 1) (pr (fst ct) (fst cu))) shape = q ∙ keyʟ-shape-in (t ≐ u) ∙ cong (λ w → pr (# m) (pr (# 1) w)) (prʟ-fst ct cu) hE = AmbientHolds.holds B δ' zero (suc (suc (suc (suc zero)))) (suc (suc (suc (suc (suc (suc Bi)))))) m refl refl refl e = atomClause-out Ci Ti Bi 1 eqRel γ heq c (nn m) ct cu y (envSet B m) c∈ shape hy hE
两个无界量词
子取值高一个元数，而那是唯一的算术；其余就是递出周遭集合、从它把那个环境恢复出来好让 cons 读式有意义、再把那条读式在两个框架之间搬过去。
ex : Closed → Total → Ex → ∀ {m} (a' : Formula S (suc m)) → Pinned a' → Pinned (∃̇ a') ex hcl hdom hex {m} a' ia c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (∃̇ a')))) (λ { (ya , hya) → let ea = ia (keyʟ a') ya refl ka hya δ' = envSet B m ∷ ya ∷ y ∷ ca ∷ nn m ∷ c ∷ γ di = suc (suc (suc (suc zero))) bi = suc (suc (suc (suc (suc (suc Bi))))) hE = AmbientHolds.holds B δ' zero di bi m refl refl refl e = quantClause-out Ci Ti Bi 8 (body∃ Bi) γ hex c (nn m) ca y ya (envSet B m) c∈ shape hy (upS a' ya hya) hE in extensionalV (λ w → ⇔toPath (λ hw → let sy = toS y w hw bo = body∃-out Bi (sy ∷ δ') (extAt-out (suc (suc zero)) (body∃ Bi) δ' e sy hw) ae = Ambient.asEnv B δ' zero di bi m refl refl hE sy (bo .fst) in subst ⟨_⟩ (sym (Sat-mem B (∃̇ a') sy)) ( bo .fst , cond∃-in B a' sy (PT.map (λ { (x , (x∈ , (e' , (hcs , he)))) → x , x∈ , e' , ( consAtL-transport (e' ∷ x ∷ sy ∷ δ') (e' ∷ x ∷ sy ∷ []) zero (suc zero) (suc (suc zero)) zero (suc zero) (suc (suc zero)) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs , subst (λ v → ⟨ fst e' ∈ v ⟩) ea he ) }) (bo .snd)) )) (λ hw → let sw = toS (Sat B (∃̇ a')) w hw h = subst ⟨_⟩ (Sat-mem B (∃̇ a') sw) hw ae = Ambient.asEnv B δ' zero di bi m refl refl hE sw (h .fst) in extAt-in (suc (suc zero)) (body∃ Bi) δ' e sw (body∃-in Bi (sw ∷ δ') (h .fst) (PT.map (λ { (x , (x∈ , (e' , (hcs , he)))) → x , x∈ , e' , ( consAtL-transport (e' ∷ x ∷ sw ∷ []) (e' ∷ x ∷ sw ∷ δ') zero (suc zero) (suc (suc zero)) zero (suc zero) (suc (suc zero)) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs , subst (λ v → ⟨ fst e' ∈ v ⟩) (sym ea) he ) }) (cond∃-out B a' sw (h .snd)))))) }) (domAt-in Ti Ci γ hdom (keyʟ a') ka) where ca : S ca = LCode.⌜ a' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 8) (fst ca)) shape = q ∙ keyʟ-shape-in (∃̇ a') ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkeyS a') (unSuccClosed-out Ci 8 γ (hcl .snd .snd .snd .snd .fst) c (nn m) ca c∈ shape) all : Closed → Total → All → ∀ {m} (a' : Formula S (suc m)) → Pinned a' → Pinned (∀̇ a') all hcl hdom hall {m} a' ia c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (∀̇ a')))) (λ { (ya , hya) → let ea = ia (keyʟ a') ya refl ka hya δ' = envSet B m ∷ ya ∷ y ∷ ca ∷ nn m ∷ c ∷ γ di = suc (suc (suc (suc zero))) bi = suc (suc (suc (suc (suc (suc Bi))))) hE = AmbientHolds.holds B δ' zero di bi m refl refl refl e = quantClause-out Ci Ti Bi 9 (body∀ Bi) γ hall c (nn m) ca y ya (envSet B m) c∈ shape hy (upS a' ya hya) hE in extensionalV (λ w → ⇔toPath (λ hw → let sy = toS y w hw bo = body∀-out Bi (sy ∷ δ') (extAt-out (suc (suc zero)) (body∀ Bi) δ' e sy hw) ae = Ambient.asEnv B δ' zero di bi m refl refl hE sy (bo .fst) in subst ⟨_⟩ (sym (Sat-mem B (∀̇ a') sy)) ( bo .fst , cond∀-in B a' sy (λ x e' x∈ hcs → subst (λ v → ⟨ fst e' ∈ v ⟩) ea (bo .snd x e' x∈ (consAtL-transport (e' ∷ x ∷ sy ∷ []) (e' ∷ x ∷ sy ∷ δ') zero (suc zero) (suc (suc zero)) zero (suc zero) (suc (suc zero)) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs))) )) (λ hw → let sw = toS (Sat B (∀̇ a')) w hw h = subst ⟨_⟩ (Sat-mem B (∀̇ a') sw) hw ae = Ambient.asEnv B δ' zero di bi m refl refl hE sw (h .fst) in extAt-in (suc (suc zero)) (body∀ Bi) δ' e sw (body∀-in Bi (sw ∷ δ') (h .fst) (λ x e' x∈ hcs → subst (λ v → ⟨ fst e' ∈ v ⟩) (sym ea) (cond∀-out B a' sw (h .snd) x e' x∈ (consAtL-transport (e' ∷ x ∷ sw ∷ δ') (e' ∷ x ∷ sw ∷ []) zero (suc zero) (suc (suc zero)) zero (suc zero) (suc (suc zero)) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs)))))) }) (domAt-in Ti Ci γ hdom (keyʟ a') ka) where ca : S ca = LCode.⌜ a' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 9) (fst ca)) shape = q ∙ keyʟ-shape-in (∀̇ a') ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkeyS a') (unSuccClosed-out Ci 9 γ (hcl .snd .snd .snd .snd .snd .fst) c (nn m) ca c∈ shape)
两个有界量词
最后两条，而它们里面的一切都已出现过：高一元数的子取值、递出的周遭集合、恢复出的环境、搬过去的 cons 读式，以及经桥读出的界项取值。成员两侧都是取自载体、由界设防，而那正是存在性那一半在试图证明这同一件事时找出的那处更正。
allIn : Closed → Total → AllIn → ∀ {m} (t : Term S m) (a' : Formula S (suc m)) → Pinned a' → Pinned (∀̇∈ t a') allIn hcl hdom hall {m} t a' ia c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (∀̇∈ t a')))) (λ { (yb , hyb) → let eb = ia (keyʟ a') yb refl ka hyb δ' = envSet B m ∷ yb ∷ y ∷ ca ∷ ct ∷ nn m ∷ c ∷ γ di = suc (suc (suc (suc (suc zero)))) bi = suc (suc (suc (suc (suc (suc (suc Bi)))))) hE = AmbientHolds.holds B δ' zero di bi m refl refl refl e = bndClause-out Ci Ti Bi 10 (bodyAll Bi) γ hall c (nn m) ct ca y yb (envSet B m) c∈ shape hy (upS a' yb hyb) hE in extensionalV (λ w → ⇔toPath (λ hw → let sy = toS y w hw bo = bodyAll-out Bi (sy ∷ δ') (extAt-out (suc (suc zero)) (bodyAll Bi) δ' e sy hw) ae = Ambient.asEnv B δ' zero di bi m refl refl hE sy (bo .fst) in subst ⟨_⟩ (sym (Sat-mem B (∀̇∈ t a') sy)) ( bo .fst , cond∀∈-in B t a' sy (λ v hv x e' x∈B x∈v hcs → subst (λ u → ⟨ fst e' ∈ u ⟩) eb (bo .snd v (termAgree t (v ∷ sy ∷ δ') ai6 ai1 ai0 (v ∷ sy ∷ []) ai0 ai1 refl refl refl .snd hv) x e' x∈B x∈v (consAtL-transport (e' ∷ x ∷ v ∷ sy ∷ []) (e' ∷ x ∷ v ∷ sy ∷ δ') zero (suc zero) (suc (suc (suc zero))) zero (suc zero) (suc (suc (suc zero))) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs))) )) (λ hw → let sw = toS (Sat B (∀̇∈ t a')) w hw h = subst ⟨_⟩ (Sat-mem B (∀̇∈ t a') sw) hw ae = Ambient.asEnv B δ' zero di bi m refl refl hE sw (h .fst) in extAt-in (suc (suc zero)) (bodyAll Bi) δ' e sw (bodyAll-in Bi (sw ∷ δ') (h .fst) (λ v hv x e' x∈B x∈v hcs → subst (λ u → ⟨ fst e' ∈ u ⟩) (sym eb) (cond∀∈-out B t a' sw (h .snd) v (termAgree t (v ∷ sw ∷ δ') ai6 ai1 ai0 (v ∷ sw ∷ []) ai0 ai1 refl refl refl .fst hv) x e' x∈B x∈v (consAtL-transport (e' ∷ x ∷ v ∷ sw ∷ δ') (e' ∷ x ∷ v ∷ sw ∷ []) zero (suc zero) (suc (suc (suc zero))) zero (suc zero) (suc (suc (suc zero))) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs)))))) }) (domAt-in Ti Ci γ hdom (keyʟ a') ka) where ct ca : S ct = LCode.⌜ t ⌝ᵗ ca = LCode.⌜ a' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 10) (pr (fst ct) (fst ca))) shape = q ∙ keyʟ-shape-in (∀̇∈ t a') ∙ cong (λ w → pr (# m) (pr (# 10) w)) (prʟ-fst ct ca) ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkeyS a') (binSuccClosed-out Ci 10 γ (hcl .snd .snd .snd .snd .snd .snd .fst) c (nn m) ct ca c∈ shape) exIn : Closed → Total → ExIn → ∀ {m} (t : Term S m) (a' : Formula S (suc m)) → Pinned a' → Pinned (∃̇∈ t a') exIn hcl hdom hex {m} t a' ia c y q c∈ hy = PT.rec (setIsSet (fst y) (fst (Sat B (∃̇∈ t a')))) (λ { (yb , hyb) → let eb = ia (keyʟ a') yb refl ka hyb δ' = envSet B m ∷ yb ∷ y ∷ ca ∷ ct ∷ nn m ∷ c ∷ γ di = suc (suc (suc (suc (suc zero)))) bi = suc (suc (suc (suc (suc (suc (suc Bi)))))) hE = AmbientHolds.holds B δ' zero di bi m refl refl refl e = bndClause-out Ci Ti Bi 11 (bodyEx Bi) γ hex c (nn m) ct ca y yb (envSet B m) c∈ shape hy (upS a' yb hyb) hE in extensionalV (λ w → ⇔toPath (λ hw → let sy = toS y w hw bo = bodyEx-out Bi (sy ∷ δ') (extAt-out (suc (suc zero)) (bodyEx Bi) δ' e sy hw) ae = Ambient.asEnv B δ' zero di bi m refl refl hE sy (bo .fst) in subst ⟨_⟩ (sym (Sat-mem B (∃̇∈ t a') sy)) ( bo .fst , cond∃∈-in B t a' sy (PT.map (λ { (v , (hv , hx)) → v , ( termAgree t (v ∷ sy ∷ δ') ai6 ai1 ai0 (v ∷ sy ∷ []) ai0 ai1 refl refl refl .fst hv , PT.map (λ { (x , (gd , (e' , (hcs , he)))) → x , (gd , (e' , ( consAtL-transport (e' ∷ x ∷ v ∷ sy ∷ δ') (e' ∷ x ∷ v ∷ sy ∷ []) zero (suc zero) (suc (suc (suc zero))) zero (suc zero) (suc (suc (suc zero))) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs , subst (λ u → ⟨ fst e' ∈ u ⟩) eb he ))) }) hx ) }) (bo .snd)) )) (λ hw → let sw = toS (Sat B (∃̇∈ t a')) w hw h = subst ⟨_⟩ (Sat-mem B (∃̇∈ t a') sw) hw ae = Ambient.asEnv B δ' zero di bi m refl refl hE sw (h .fst) in extAt-in (suc (suc zero)) (bodyEx Bi) δ' e sw (bodyEx-in Bi (sw ∷ δ') (h .fst) (PT.map (λ { (v , (hv , hx)) → v , ( termAgree t (v ∷ sw ∷ δ') ai6 ai1 ai0 (v ∷ sw ∷ []) ai0 ai1 refl refl refl .snd hv , PT.map (λ { (x , (gd , (e' , (hcs , he)))) → x , (gd , (e' , ( consAtL-transport (e' ∷ x ∷ v ∷ sw ∷ []) (e' ∷ x ∷ v ∷ sw ∷ δ') zero (suc zero) (suc (suc (suc zero))) zero (suc zero) (suc (suc (suc zero))) (λ i → ⟪ fst B ⟫↪ (ae .fst i)) (ae .snd) refl refl refl hcs , subst (λ u → ⟨ fst e' ∈ u ⟩) (sym eb) he ))) }) hx ) }) (cond∃∈-out B t a' sw (h .snd)))))) }) (domAt-in Ti Ci γ hdom (keyʟ a') ka) where ct ca : S ct = LCode.⌜ t ⌝ᵗ ca = LCode.⌜ a' ⌝ shape : fst c ≡ pr (fst (nn m)) (pr (# 11) (pr (fst ct) (fst ca))) shape = q ∙ keyʟ-shape-in (∃̇∈ t a') ∙ cong (λ w → pr (# m) (pr (# 11) w)) (prʟ-fst ct ca) ka : ⟨ fst (keyʟ a') ∈ fst C ⟩ ka = subst (λ w → ⟨ w ∈ fst C ⟩) (kkeyS a') (binSuccClosed-out Ci 11 γ (hcl .snd .snd .snd .snd .snd .snd .snd) c (nn m) ct ca c∈ shape)
那次归纳
十二种情形，以及把它们系在一起、沿公式的那次递归。这就是唯一性那一半的全部：一张封闭、全、且满足十二条的表，在每个键处记录的都是元语言递归在那里造出的取值。
Clauses : Type (ℓ-suc ℓ) Clauses = Mem × (Eq × (And × (Or × (Imp × (Neg × (Top × (Bot × (Ex × (All × (AllIn × ExIn)))))))))) pinned : Closed → Total → Clauses → ∀ {m} (ψ : Formula S m) → Pinned ψ pinned hc hd h (t ∈̇ u) = mem (h .fst) t u pinned hc hd h (t ≐ u) = eq (h .snd .fst) t u pinned hc hd h (a ∧̇ b) = and hc hd (h .snd .snd .fst) a b (pinned hc hd h a) (pinned hc hd h b) pinned hc hd h (a ∨̇ b) = or hc hd (h .snd .snd .snd .fst) a b (pinned hc hd h a) (pinned hc hd h b) pinned hc hd h (a ⇒̇ b) = imp hc hd (h .snd .snd .snd .snd .fst) a b (pinned hc hd h a) (pinned hc hd h b) pinned hc hd h (¬̇ a) = neg hc hd (h .snd .snd .snd .snd .snd .fst) a (pinned hc hd h a) pinned hc hd h ⊤̇ = top (h .snd .snd .snd .snd .snd .snd .fst) pinned hc hd h ⊥̇ = bot (h .snd .snd .snd .snd .snd .snd .snd .fst) pinned hc hd h (∃̇ a) = ex hc hd (h .snd .snd .snd .snd .snd .snd .snd .snd .fst) a (pinned hc hd h a) pinned hc hd h (∀̇ a) = all hc hd (h .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) a (pinned hc hd h a) pinned hc hd h (∀̇∈ t a) = allIn hc hd (h .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) t a (pinned hc hd h a) pinned hc hd h (∃̇∈ t a) = exIn hc hd (h .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd) t a (pinned hc hd h a)