BedrockA good table has only one value
The uniqueness half. A table that satisfies the twelve clauses over a subcode-closed index set, and answers at every key in it, records at each key the value the meta-level recursion built there, and nothing else. That is what makes the graph single-valued.
It is stated against the canonical value rather than between two arbitrary tables. The two forms are the same induction, and the pinned one is shorter and is the one a recursion consumes: what funct needs is that the value at an index is determined, and the meta-level recursion is where a determined value comes from.
The statement's shape is not a matter of taste. The index and the value are variables and the key is reached by an equation, exactly as every clause reader is written; stating a case at a key already substituted in puts two concrete set constructions inside a satisfaction, and that does not typecheck in any reasonable time. This chapter learned that at its first case.
{-# 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
What a good table is
Three things, in the order the graph will state them: the index set holds the subcodes of its members, the table answers at every index, and the twelve clauses hold. The first two are what the existence half had to build; here they are hypotheses, because the table is now arbitrary.
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 ψ)
The constant that pins itself
The first case, and the one that needs nothing: the clause for ⊥̇ says the value is empty, the recursion cut its value out of the ambient set by a condition nothing satisfies, and two empty sets are equal. No ambient set has to be supplied, no subvalue exists to replace, and no induction hypothesis is used.
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
The constant the ambient set pins
The second constant, and the first case that has to supply an ambient set rather than consume one. The clause says the value is the set of environments; the recursion cut its value out of that set by a condition everything satisfies, so the value is that set again. The supplying is one application of the agreement, and the arities and the carrier match by refl because the frame put them where the clause looks.
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})))
The first case with an induction hypothesis
Conjunction, and with it the shape the remaining ten follow. Closedness puts the subkeys in the index, totality gives the table an entry at each of them, the induction hypothesis says those entries are the recursion's values, the clause says the value at the key is their intersection, and the recursion cut its value out by the same condition. The entries arrive merely, which costs nothing, because the goal is an equation between sets.
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
Negation, the last new combination
The three ingredients at once: an ambient set to supply, a subvalue to identify, and an induction hypothesis to use. Every remaining case is one of these with a different clause, and none needs a fourth ingredient.
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)
Implication
Two subvalues and an ambient set, which is negation and conjunction at once. The identity is the object language's own arrow on both sides, which is the choice the chapter that wrote the clauses made and had to make: the joined form would need the excluded middle, and neither chapter takes it.
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
The atoms
An atom has no subformula, so it needs neither closedness nor the induction hypothesis: an ambient set to supply, and the term bridge twice. The clause reads the two values off the codes, the recursion reads them off the terms, and the bridge says they agree.
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
The unbounded quantifiers
The subvalue sits an arity up, which is the only arithmetic; the rest is the ambient set supplied, the environment recovered from it so the cons reader means something, and that reader carried between the two frames.
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)
The bounded quantifiers
The last two, and everything in them has appeared already: the subvalue an arity up, the ambient set supplied, the environment recovered, the cons reader carried, and the bound term's value read through the bridge. The member is drawn from the carrier and guarded by the bound on both sides, which is the correction the existence half found by trying to prove exactly this.
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)
The induction
Twelve cases and the recursion over the formula that ties them together. This is the uniqueness half entire: a table that is closed, total and satisfies the twelve records at every key the value the meta-level recursion built there.
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)