BedrockThe graph
What the recursion's graph says: there is an index set holding the subcodes of its members, a table answering at every index and satisfying the twelve clauses, and the value is what that table records at this index.
The index set and the table are bound because a graph may not name a table it has not been given, which is the one thing the internalization theorem forbids: the recursion is what produces the table, so the graph that defines it must quantify over tables rather than point at one.
The carrier is bound for a different reason, and that reason is why the chapter is one frame with two instances. Every clause takes the carrier as a slot and none takes it as a term, so something has to occupy that slot, and what may occupy it depends on the caller. A caller holding the carrier as a set of its own pins a bound variable to a constant. A caller whose carrier is itself a bound variable, which is exactly what a stage of the internal hierarchy is, has no constant to pin it to, because a set enters a formula only by being named. So the pinning clause is the frame's parameter, and the two instances are the two clauses that fit it.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.Graph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( closedAt; domAt; appAt; appAt-adequate ; memClauseAt; eqClauseAt; andClauseAt; orClauseAt; impClauseAt ; negClauseAt; topClauseAt; botClauseAt; existClauseAt; forallClauseAt ; allInClauseAt; exInClauseAt ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
The twelve, and the three that guard them
The clauses take their three slots as arguments, and conjoining them is the whole of this section. The three hypotheses without which they say nothing come with them: a table with one entry at a compound code satisfies all twelve, so closedness and totality are not decoration.
The frame binds the index set, the table and the carrier, in that order, and opens with whatever clause pins the last of them. Nothing below the pin varies between the instances: the same three guards and the same twelve, at the same three slots, with the two free slots shifted past the three binders.
private Ci Ti Bi : ∀ {n} → Fin (suc (suc (suc n))) Ci = suc (suc zero) Ti = suc zero Bi = zero sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i)) twelveAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n twelveAt C T B = memClauseAt C T B ∧̇ (eqClauseAt C T B ∧̇ (andClauseAt C T ∧̇ (orClauseAt C T ∧̇ (impClauseAt C T B ∧̇ (negClauseAt C T B ∧̇ (topClauseAt C T B ∧̇ (botClauseAt C T ∧̇ (existClauseAt C T B ∧̇ (forallClauseAt C T B ∧̇ (allInClauseAt C T B ∧̇ exInClauseAt C T B)))))))))) private satGraphOn : ∀ {n} → Formula S (suc (suc (suc n))) → Fin n → Fin n → Formula S n satGraphOn pin x y = ∃̇ (∃̇ (∃̇ ( pin ∧̇ ( closedAt Ci ∧̇ ( domAt Ti Ci ∧̇ ( appAt Ti (sh3 x) (sh3 y) ∧̇ twelveAt Ci Ti Bi ))))))
What a witness is
Three nested existentials, read flat, at a variable environment and at a carrier handed over as an element. The reading is stated at variable arguments, which is what keeps a proof that supplies or consumes a witness from substituting under three binders at concrete sets, and the environment is a variable for the same reason: a consumer that wants the carrier as a slot has no concrete environment to offer.
The pin is the one component the frame cannot read by itself, so it takes that reading as a hypothesis, one direction per reading. At both instances the hypothesis is the identity, because a variable equated to a constant and a variable equated to a variable read as the same equation between underlying sets.
private GraphWitOn : ∀ {n} → S → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) GraphWitOn W x y γ = Σ[ C ∈ S ] (Σ[ T ∈ S ] (Σ[ b ∈ S ] ((fst b ≡ fst W) × (⟨ (b ∷ T ∷ C ∷ γ) ⊨ closedAt Ci ⟩ × (⟨ (b ∷ T ∷ C ∷ γ) ⊨ domAt Ti Ci ⟩ × (⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst T ⟩ × ⟨ (b ∷ T ∷ C ∷ γ) ⊨ twelveAt Ci Ti Bi ⟩)))))) module _ {n : ℕ} (pin : Formula S (suc (suc (suc n)))) (W : S) (x y : Fin n) (γ : S ^ n) where graphOn-in : ((b T C : S) → fst b ≡ fst W → ⟨ (b ∷ T ∷ C ∷ γ) ⊨ pin ⟩) → ∥ GraphWitOn W x y γ ∥₁ → ⟨ γ ⊨ satGraphOn pin x y ⟩ graphOn-in rd = PT.map (λ { (C , (T , (b , (eb , (hc , (hd , (ha , h12))))))) → C , ∣ T , ∣ b , (rd b T C eb , (hc , (hd , ( subst ⟨_⟩ (sym (appAt-adequate Ti (sh3 x) (sh3 y) (b ∷ T ∷ C ∷ γ))) ha , h12 )))) ∣₁ ∣₁ }) graphOn-out : ((b T C : S) → ⟨ (b ∷ T ∷ C ∷ γ) ⊨ pin ⟩ → fst b ≡ fst W) → ⟨ γ ⊨ satGraphOn pin x y ⟩ → ∥ GraphWitOn W x y γ ∥₁ graphOn-out rd = PT.rec squash₁ (λ { (C , hT) → PT.rec squash₁ (λ { (T , hb) → PT.map (λ { (b , (eb , (hc , (hd , (ha , h12))))) → C , (T , (b , (rd b T C eb , (hc , (hd , ( subst ⟨_⟩ (appAt-adequate Ti (sh3 x) (sh3 y) (b ∷ T ∷ C ∷ γ)) ha , h12 )))))) }) hb }) hT })
The carrier as a slot
The general instance, and the one the internal hierarchy will use. The pin equates the graph's own bound carrier to whatever the ambient environment holds at the given slot, and the witness says which set that is by looking the slot up. Nothing here is a set the formula names, so a caller may put the graph under as many binders as it likes.
satGraphAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n satGraphAt B x y = satGraphOn (var Bi ≐ var (sh3 B)) x y GraphWitAt : ∀ {n} → Fin n → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) GraphWitAt B x y γ = GraphWitOn (lookup B γ) x y γ graphAt-in : ∀ {n} (B x y : Fin n) (γ : S ^ n) → ∥ GraphWitAt B x y γ ∥₁ → ⟨ γ ⊨ satGraphAt B x y ⟩ graphAt-in B x y γ = graphOn-in (var Bi ≐ var (sh3 B)) (lookup B γ) x y γ (λ _ _ _ e → e) graphAt-out : ∀ {n} (B x y : Fin n) (γ : S ^ n) → ⟨ γ ⊨ satGraphAt B x y ⟩ → ∥ GraphWitAt B x y γ ∥₁ graphAt-out B x y γ = graphOn-out (var Bi ≐ var (sh3 B)) (lookup B γ) x y γ (λ _ _ _ h → h)
The carrier as a constant
The same frame with the constant in place of the slot, at two free variables, and this is the form the per-formula recursion and the recursion over a stage's codes both consume. It is delivered at the types it had before the frame existed, and its witness type is the same tuple in the same order at the same environment, so nothing that builds or reads one has anything to notice.
satGraph : S → Formula S 2 satGraph B = satGraphOn (var Bi ≐ con B) (suc zero) zero GraphWit : (B x y : S) → Type (ℓ-suc ℓ) GraphWit B x y = GraphWitOn B (suc zero) zero (y ∷ x ∷ []) graph-in : (B x y : S) → ∥ GraphWit B x y ∥₁ → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ graph-in B x y = graphOn-in (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ e → e) graph-out : (B x y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → ∥ GraphWit B x y ∥₁ graph-out B x y = graphOn-out (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ h → h)