The object language over the model

The readers were written about the hierarchy and the bridge carries them into the model. This chapter takes the bridge across, once, and states what a quoted reader means on the far side.

There is one wrinkle and it is small. A reader's meaning was stated in terms of the value of a variable in a hierarchy environment; on the far side the environment holds elements of the model, and the hierarchy environment is the one obtained by taking underlying sets. Looking up in the projected environment is projecting the lookup, which is a two-line induction, and after it the quoted reader says exactly what the original said about the underlying sets.

The first reader to cross is the one everything else is built from: the ordered pair. Nothing above it needs a new argument, because the bridge is generic and the readers' own characterizations were proved once already.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth

module L.Coding.Model {ℓ : 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
import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import V.Model {ℓ} using ( pair-singleton )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import FOL.Manipulation.Bounding using ( BoundedFo )
open import L.Absoluteness {ℓ} using ( InL; liftFo; transferFo )
open import L.Coding.Base {ℓ}
  using ( prAt; Δ₀-prAt; prAt-adequate; sglConAt; pairConAt; tagAt )
open import L.Coding.Environment {ℓ}
  using ( sucAt; Δ₀-sucAt; sucAt-adequate; consAt; Δ₀-consAt; consAt-adequate
        ; env; cons; shiftPairAt )
open import L.Axioms.Numerals {ℓ}
  using ( numeralL; numeralL-fst; pairʟ; pairʟ-fst; sucʟ; sucʟ-fst )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Vec using ( map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ using ( S )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

Looking up in a projected environment

Two lines, and the only bookkeeping the crossing costs.

lookup-fst : ∀ {n} (i : Fin n) (γ : S ^ n)
           → lookup i (map fst γ) ≡ fst (lookup i γ)
lookup-fst zero    (x ∷ γ) = refl
lookup-fst (suc i) (x ∷ γ) = lookup-fst i γ

The ordered pair

The quoted reader is the original lifted along the bridge, and the lift asks for nothing: the reader names no constants, so there is nothing to be constructible and the admissibility witness is empty.

Its meaning is three steps. The bridge equates satisfaction in the model with satisfaction in the hierarchy at the projected environment; the reader's own characterization says what that is; and the lookups are projected. What comes out is the statement a consumer wants: the value of one variable is the Kuratowski pair of the values of the other two, as sets.

private
  PairIs : V ℓ → V ℓ → Ω
  PairIs a p = (a ≡ p) , setIsSet a p

prAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
prAtL q u v = liftFo (prAt q u v) _

prAtL-adequate : ∀ {n} (q u v : Fin n) (γ : S ^ n)
  → (γ ⊨ prAtL q u v)
  ≡ PairIs (fst (lookup q γ)) (pr (fst (lookup u γ)) (fst (lookup v γ)))
prAtL-adequate q u v γ =
    transferFo (prAt q u v) _ (Δ₀-prAt q u v) γ
  ∙ prAt-adequate q u v (map fst γ)
  ∙ cong₂ PairIs (lookup-fst q γ)
      (cong₂ pr (lookup-fst u γ) (lookup-fst v γ))

Application

A function in the object language is a set of ordered pairs, so the one thing every use of one asks is whether a given pair belongs to it. That is a bounded existential over the function, with the pair reader inside, and its meaning is membership of the Kuratowski pair.

The backward direction is where the model earns its keep, and it is worth noticing. To satisfy the existential one must produce an element of the model whose underlying set is the pair; the hypothesis only supplies a set. It is constructible because it belongs to something constructible, and the class is transitive. That is the whole argument, and the same step will recur wherever a witness has to be produced inside the model rather than merely in the hierarchy.

appAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
appAt f x y = ∃̇∈ (var f) (prAtL zero (suc x) (suc y))

appAt-adequate : ∀ {n} (f x y : Fin n) (γ : S ^ n)
  → (γ ⊨ appAt f x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (lookup f γ))
appAt-adequate f x y γ = ⇔toPath fwd bwd
  where
  a = fst (lookup x γ)
  b = fst (lookup y γ)
  F = lookup f γ

  read : (z : S) → ⟨ (z ∷ γ) ⊨ prAtL zero (suc x) (suc y) ⟩ → fst z ≡ pr a b
  read z h = subst ⟨_⟩ (prAtL-adequate zero (suc x) (suc y) (z ∷ γ)) h

  fwd : ⟨ γ ⊨ appAt f x y ⟩ → ⟨ pr a b ∈ fst F ⟩
  fwd = PT.rec (snd (pr a b ∈ fst F))
    (λ { (z , (z∈F , h)) → subst (λ w → ⟨ w ∈ fst F ⟩) (read z h) z∈F })

  bwd : ⟨ pr a b ∈ fst F ⟩ → ⟨ γ ⊨ appAt f x y ⟩
  bwd h = ∣ zS , (h , subst ⟨_⟩
      (sym (prAtL-adequate zero (suc x) (suc y) (zS ∷ γ))) refl) ∣₁
    where
    zS : S
    zS = pr a b , isL-trans {x = fst F} {y = pr a b} h (F .snd)

Single-valuedness

The other half of being a function: a pair's first component determines its second. Three unbounded quantifiers, which cost nothing here, and two applications of the reader above.

Stated as two directions rather than a path, because that is how consumers use it and because building the right-hand side as a proposition would say the same thing at more length. Reading it out is the direction that matters: from the object-language claim, an actual proof that two values recorded against the same argument agree.

svAt : ∀ {n} → Fin n → Formula S n
svAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero)
  ⇒̇ (appAt (suc (suc (suc f))) (suc (suc zero)) zero
  ⇒̇ (var (suc zero) ≐ var zero)))))

module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds : S → S → Type (ℓ-suc ℓ)
    Holds x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at : (x y y' : S)
       → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero))
       ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero)
                  (y' ∷ y ∷ x ∷ γ)

    at' : (x y y' : S)
        → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) zero)
        ≡ (pr (fst x) (fst y') ∈ fst (lookup f γ))
    at' x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) zero
                   (y' ∷ y ∷ x ∷ γ)

  svAt-out : ⟨ γ ⊨ svAt f ⟩
           → (x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y'
  svAt-out h x y y' p q = h x y y'
    (subst ⟨_⟩ (sym (at x y y')) p) (subst ⟨_⟩ (sym (at' x y y')) q)

  svAt-in : ((x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y')
          → ⟨ γ ⊨ svAt f ⟩
  svAt-in h x y y' p q = h x y y'
    (subst ⟨_⟩ (at x y y') p) (subst ⟨_⟩ (at' x y y') q)

The domain

Being in the domain is having a value: one unbounded existential over the reader above. The domain itself is then the set with exactly those members, said as two implications, since the object language has no biconditional of its own and spelling it out is shorter than adding one.

Both are used in one direction each, and only those directions are extracted. A consumer holding a table asks either "this argument has an entry, so it is in the domain" or "this argument is in the domain, so it has an entry"; nothing wants the statement as a proposition.

inDomAt : ∀ {n} → Fin n → Fin n → Formula S n
inDomAt f x = ∃̇ (appAt (suc f) (suc x) zero)

inDomAt-adequate : ∀ {n} (f x : Fin n) (γ : S ^ n)
  → (γ ⊨ inDomAt f x)
  ≡ (∃[ y ∶ S ] (pr (fst (lookup x γ)) (fst y) ∈ fst (lookup f γ)))
inDomAt-adequate f x γ =
  cong (⋁ S) (funExt (λ y → appAt-adequate (suc f) (suc x) zero (y ∷ γ)))

domAt : ∀ {n} → Fin n → Fin n → Formula S n
domAt f d = ∀̇ ( (inDomAt (suc f) zero ⇒̇ (var zero ∈̇ var (suc d)))
             ∧̇ ((var zero ∈̇ var (suc d)) ⇒̇ inDomAt (suc f) zero) )

module _ {n : ℕ} (f d : Fin n) (γ : S ^ n) where
  private
    step : (x : S)
         → ((x ∷ γ) ⊨ inDomAt (suc f) zero)
         ≡ (∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)))
    step x = inDomAt-adequate (suc f) zero (x ∷ γ)

  domAt-out : ⟨ γ ⊨ domAt f d ⟩ → (x y : S)
            → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
            → ⟨ fst x ∈ fst (lookup d γ) ⟩
  domAt-out h x y p = h x .fst (subst ⟨_⟩ (sym (step x)) ∣ y , p ∣₁)

  domAt-in : ⟨ γ ⊨ domAt f d ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩
           → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁
  domAt-in h x m = subst ⟨_⟩ (step x) (h x .snd m)

  domAt-intro : ((x : S)
                 → (⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩
                    → ⟨ fst x ∈ fst (lookup d γ) ⟩)
                 × (⟨ fst x ∈ fst (lookup d γ) ⟩
                    → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩))
              → ⟨ γ ⊨ domAt f d ⟩
  domAt-intro g x = (λ h → g x .fst (subst ⟨_⟩ (step x) h))
                  , (λ m → subst ⟨_⟩ (sym (step x)) (g x .snd m))

The pair, inside the model

Every code is built by pairing, so every construction below needs the ordered pair of two elements of L to be one. It is, three applications of the model's own pairing, and the projection equations of the numeral chapter say that reading it through the underlying set gives the hierarchy's pair back. The singleton is the two-element pair with equal components, which is the one small identity the hierarchy supplies.

prʟ : S → S → S
prʟ a b = pairʟ (pairʟ a a) (pairʟ a b)

prʟ-fst : (a b : S) → fst (prʟ a b) ≡ pr (fst a) (fst b)
prʟ-fst a b =
    pairʟ-fst (pairʟ a a) (pairʟ a b)
  ∙ cong₂ ⁅_,_⁆ (pairʟ-fst a a ∙ pair-singleton (fst a)) (pairʟ-fst a b)

The coding, at the model

The pair and the numerals are injective, which is everything the coding chapter asks of a structure, so the object language codes into L itself. Two things follow and both are wanted. A code is an element of the model by construction, with no constructibility certificate to carry or to prove. And the code equation is injective at this arity, by the chapter's own theorem, which is what a table indexed by codes needs: two occurrences of different subformulas must not share a key, or the table is multi-valued and its existence fails.

The bridge says the two codings agree: reading a code of the model through the underlying set gives the hierarchy's code of the relabelled formula. Twelve clauses and two, each one tag equation over the clause below it. It is what lets the readers of this chapter, which are written on the hierarchy side, be applied to codes built on the model side.

prʟ-inj : {a b c d : S} → prʟ a b ≡ prʟ c d → (a ≡ c) × (b ≡ d)
prʟ-inj {a} {b} {c} {d} e =
    Σ≡Prop (λ v → snd (isL v)) (pr-inj q .fst)
  , Σ≡Prop (λ v → snd (isL v)) (pr-inj q .snd)
  where
  q : pr (fst a) (fst b) ≡ pr (fst c) (fst d)
  q = sym (prʟ-fst a b) ∙ cong fst e ∙ prʟ-fst c d

numeralL-inj : {j k : ℕ} → numeralL j ≡ numeralL k → j ≡ k
numeralL-inj {j} {k} e =
  #-inj′ (sym (numeralL-fst j) ∙ cong fst e ∙ numeralL-fst k)

module LCode = FOL.Coding {ℓ-suc ℓ} 𝒮ʟ prʟ prʟ-inj numeralL numeralL-inj

tagBridge : (k : ℕ) (x : S) → fst (LCode.mkTag k x) ≡ VCode.mkTag k (fst x)
tagBridge k x = prʟ-fst (numeralL k) x ∙ cong₂ pr (numeralL-fst k) refl

codeBridgeTm : ∀ {n} (t : Term S n) → fst LCode.⌜ t ⌝ᵗ ≡ VCode.⌜ mapTm fst t ⌝ᵗ
codeBridgeTm (con c) = tagBridge  c
codeBridgeTm (var i) =
  tagBridge  (numeralL (toℕ i)) ∙ cong (VCode.mkTag ) (numeralL-fst (toℕ i))

codeBridge : ∀ {n} (φ : Formula S n) → fst LCode.⌜ φ ⌝ ≡ VCode.⌜ mapFo fst φ ⌝
codeBridge (t ∈̇ u) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (t ≐ u) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (a ∧̇ b) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ∨̇ b) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ⇒̇ b) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (¬̇ a)   = tagBridge  _ ∙ cong (VCode.mkTag ) (codeBridge a)
codeBridge ⊤̇       = tagBridge  _ ∙ cong (VCode.mkTag ) (numeralL-fst )
codeBridge ⊥̇       = tagBridge  _ ∙ cong (VCode.mkTag ) (numeralL-fst )
codeBridge (∃̇ a)   = tagBridge  _ ∙ cong (VCode.mkTag ) (codeBridge a)
codeBridge (∀̇ a)   = tagBridge  _ ∙ cong (VCode.mkTag ) (codeBridge a)
codeBridge (∀̇∈ t a) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
codeBridge (∃̇∈ t a) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))

Environments

An environment is a function whose values lie in a given set, so an environment over a set is the conjunction of four things: single-valued, with the given domain, with values where they belong, and made of pairs.

The fourth is easy to leave out and fatal to leave out. The other three all speak about the pairs in a set and say nothing whatever about a member that is not one, so without it a set could carry any amount of junk and still qualify. That costs nothing where the predicate is only tested, but the frame that describes a set by its members asserts both directions, so a value satisfying it would have to contain every such junk-bearing set: a proper class, and a hypothesis no set can discharge. The conjunct pins each member to a pair of an index and a value, which makes an environment a subset of a product and the collection of them a set.

Only the four projections are given, because that is all a consumer wants. Whether a particular set is the set of all environments of a given length is a different question, and a harder one; this says only what it means for a single thing to be one.

valuesInAt : ∀ {n} → Fin n → Fin n → Formula S n
valuesInAt f B = ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero
                     ⇒̇ (var zero ∈̇ var (suc (suc B))) ))

valuesInAt-out : ∀ {n} (f B : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ valuesInAt f B ⟩ → (x y : S)
               → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
               → ⟨ fst y ∈ fst (lookup B γ) ⟩
valuesInAt-out f B γ h x y p = h x y
  (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ))) p)

pairsInAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
pairsInAt e d B =
  ∀̇∈ (var e) (∃̇∈ (var (suc d)) (∃̇∈ (var (suc (suc B)))
    (prAtL (suc (suc zero)) (suc zero) zero)))

pairsIn-out : ∀ {n} (e d B : Fin n) (γ : S ^ n) → ⟨ γ ⊨ pairsInAt e d B ⟩
            → (s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
            → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                  (⟨ fst u ∈ fst (lookup d γ) ⟩
                   × (⟨ fst v ∈ fst (lookup B γ) ⟩
                      × (fst s ≡ pr (fst u) (fst v)))))) ∥₁
pairsIn-out e d B γ h s s∈ = PT.rec squash₁
  (λ { (u , (u∈ , hv)) → PT.map
    (λ { (v , (v∈ , hp)) → u , (v , (u∈ , (v∈ , subst ⟨_⟩
      (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ)) hp))) })
    hv })
  (h s s∈)

pairsIn-in : ∀ {n} (e d B : Fin n) (γ : S ^ n)
           → ((s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
              → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                    (⟨ fst u ∈ fst (lookup d γ) ⟩
                     × (⟨ fst v ∈ fst (lookup B γ) ⟩
                        × (fst s ≡ pr (fst u) (fst v)))))) ∥₁)
           → ⟨ γ ⊨ pairsInAt e d B ⟩
pairsIn-in e d B γ k s s∈ = PT.map
  (λ { (u , (v , (u∈ , (v∈ , eq)))) → u , (u∈ , ∣ v , (v∈ , subst ⟨_⟩
    (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ))) eq) ∣₁) })
  (k s s∈)

envOverAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envOverAt e d B =
  svAt e ∧̇ (domAt e d ∧̇ (valuesInAt e B ∧̇ pairsInAt e d B))

module _ {n : ℕ} (e d B : Fin n) (γ : S ^ n) (h : ⟨ γ ⊨ envOverAt e d B ⟩) where
  envOver-sv     : ⟨ γ ⊨ svAt e ⟩
  envOver-sv     = h .fst
  envOver-dom    : ⟨ γ ⊨ domAt e d ⟩
  envOver-dom    = h .snd .fst
  envOver-values : ⟨ γ ⊨ valuesInAt e B ⟩
  envOver-values = h .snd .snd .fst
  envOver-pairs  : ⟨ γ ⊨ pairsInAt e d B ⟩
  envOver-pairs  = h .snd .snd .snd

A description reads the same in any frame that puts the same three sets where it looks. Every reader above is stated through fst of a lookup and nothing else, so moving the description from one environment to another is four transports and no thought. Seven of the twelve clauses bind their own ambient set, and this is what turns "the members of that set are the environments" back into a statement about the set a construction actually built.

valuesInAt-in : ∀ {n} (f B : Fin n) (γ : S ^ n)
              → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
                 → ⟨ fst y ∈ fst (lookup B γ) ⟩)
              → ⟨ γ ⊨ valuesInAt f B ⟩
valuesInAt-in f B γ k x y hp = k x y
  (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ)) hp)

envOverAt-transport : ∀ {n n'} (γ : S ^ n) (γ' : S ^ n')
                      (e d B : Fin n) (e' d' B' : Fin n')
                    → fst (lookup e γ) ≡ fst (lookup e' γ')
                    → fst (lookup d γ) ≡ fst (lookup d' γ')
                    → fst (lookup B γ) ≡ fst (lookup B' γ')
                    → ⟨ γ ⊨ envOverAt e d B ⟩ → ⟨ γ' ⊨ envOverAt e' d' B' ⟩
envOverAt-transport γ γ' e d B e' d' B' qe qd qb h =
    svAt-in e' γ' (λ x y y' p q →
      svAt-out e γ (envOver-sv e d B γ h) x y y'
        (subst ⟨_⟩ (sym (at x y)) p) (subst ⟨_⟩ (sym (at x y')) q))
  , ( domAt-intro e' d' γ'
      (λ x → (λ m → subst (λ w → ⟨ fst x ∈ w ⟩) qd
                (PT.rec (snd (fst x ∈ fst (lookup d γ)))
                  (λ { (y , p) → domAt-out e d γ (envOver-dom e d B γ h) x y
                         (subst ⟨_⟩ (sym (at x y)) p) })
                  m))
            , (λ hx → PT.map (λ { (y , p) → y , subst ⟨_⟩ (at x y) p })
                (domAt-in e d γ (envOver-dom e d B γ h) x
                  (subst (λ w → ⟨ fst x ∈ w ⟩) (sym qd) hx))))
    , ( valuesInAt-in e' B' γ'
        (λ x y p → subst (λ w → ⟨ fst y ∈ w ⟩) qb
          (valuesInAt-out e B γ (envOver-values e d B γ h) x y
            (subst ⟨_⟩ (sym (at x y)) p)))
      , pairsIn-in e' d' B' γ'
        (λ s s∈ → PT.map
          (λ { (u , (v , (u∈ , (v∈ , eq)))) →
            u , (v , ( subst (λ w → ⟨ fst u ∈ w ⟩) qd u∈
                     , ( subst (λ w → ⟨ fst v ∈ w ⟩) qb v∈ , eq ) )) })
          (pairsIn-out e d B γ (envOver-pairs e d B γ h) s
            (subst (λ w → ⟨ fst s ∈ w ⟩) (sym qe) s∈))) ) )
  where
  at : (x y : S) → (pr (fst x) (fst y) ∈ fst (lookup e γ))
                 ≡ (pr (fst x) (fst y) ∈ fst (lookup e' γ'))
  at x y = cong (λ w → pr (fst x) (fst y) ∈ w) qe

Tags

A code carries its constructor as a numeral in the first component of a pair, so reading a code's shape means reading a pair whose first component is a given numeral. The reader for that could be quoted like the others, but it would cost more than writing it: the hierarchy's version names the numeral as a constant of the hierarchy, so the bridge would demand a constructibility witness threaded through the whole shape of the formula.

Writing it takes the shorter road, and the road the bridge chapter recommends. The numeral of L is already an element of the model, so it is already a legal constant here; one unbounded existential says "there is something equal to it, and the pair is built from that". Unbounded costs nothing, and the two readers below reuse the pair reader unchanged rather than re-deriving anything.

The second is the one that does the work later. Every binary constructor of the object language has a code of the same shape, tag applied to the pair of the two subcodes, differing only in which numeral the tag is.

tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = ∃̇ ((var zero ≐ con (numeralL k)) ∧̇ prAtL (suc s) zero (suc x))

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : S ^ n)
  → (γ ⊨ tagAtL s k x)
  ≡ PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))
tagAtL-adequate s k x γ = ⇔toPath fwd bwd
  where
  target = PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))

  fwd : ⟨ γ ⊨ tagAtL s k x ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (e , p)) →
      subst ⟨_⟩ (prAtL-adequate (suc s) zero (suc x) (z ∷ γ)) p
      ∙ cong (λ w → pr w (fst (lookup x γ))) (e ∙ numeralL-fst k) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ tagAtL s k x ⟩
  bwd q = ∣ numeralL k , (refl , subst ⟨_⟩
      (sym (prAtL-adequate (suc s) zero (suc x) (numeralL k ∷ γ)))
      (q ∙ cong (λ w → pr w (fst (lookup x γ))) (sym (numeralL-fst k)))) ∣₁

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b =
  ∃̇ (prAtL zero (suc a) (suc b) ∧̇ tagAtL (suc s) k zero)

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs (fst (lookup s γ))
      (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ))))
tagPairAtL-adequate s k a b γ = ⇔toPath fwd bwd
  where
  A = fst (lookup a γ)
  B = fst (lookup b γ)
  target = PairIs (fst (lookup s γ)) (pr (# k) (pr A B))

  fwd : ⟨ γ ⊨ tagPairAtL s k a b ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , t)) →
      subst ⟨_⟩ (tagAtL-adequate (suc s) k zero (z ∷ γ)) t
      ∙ cong (pr (# k))
          (subst ⟨_⟩ (prAtL-adequate zero (suc a) (suc b) (z ∷ γ)) p) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ tagPairAtL s k a b ⟩
  bwd q = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc a) (suc b) (zS ∷ γ))) e
      , subst ⟨_⟩ (sym (tagAtL-adequate (suc s) k zero (zS ∷ γ)))
          (q ∙ cong (pr (# k)) (sym e)) ) ∣₁
    where
    zS : S
    zS = prʟ (lookup a γ) (lookup b γ)
    e : fst zS ≡ pr A B
    e = prʟ-fst (lookup a γ) (lookup b γ)

Sets by extension

Every clause of a recursion whose values are sets says the same thing: this value is the set of exactly those things satisfying such-and-such. Written once, with the condition left as a parameter, it is two implications under one quantifier, and its two readings are the two projections. Nothing is proved, which is the point: after this the clauses of a recursion cost only their conditions.

The set operations follow immediately, each one condition long, and each with its meaning already in hand. The rest of a clause's content is whatever the condition says, and that is where the mathematics of a particular recursion lives.

extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : S ^ n) where
  extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
            → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
  extAt-out h = h .fst

  extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
           → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩
  extAt-in h = h .snd

  extAt-in-both : ((z : S) → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
                → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩)
                → ⟨ γ ⊨ extAt y φ ⟩
  extAt-in-both f g = f , g

private
  memb : ∀ {n} → Fin n → Formula S (suc n)
  memb a = var zero ∈̇ var (suc a)

interAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
interAt y a b = extAt y (memb a ∧̇ memb b)

unionAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
unionAt y a b = extAt y (memb a ∨̇ memb b)

diffAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
diffAt y a b = extAt y (memb a ∧̇ ¬̇ memb b)

sameAt : ∀ {n} → Fin n → Fin n → Formula S n
sameAt y a = extAt y (memb a)

emptyAt : ∀ {n} → Fin n → Formula S n
emptyAt y = extAt y ⊥̇

implAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
implAt y e a b = extAt y (memb e ∧̇ (memb a ⇒̇ memb b))

Reading a key in two layers

The codes a recursion ranges over carry their arity: an entry is the arity's numeral paired with the code proper, and the code proper is in turn a tag paired with its payload. So a clause's hypothesis has to read two layers, not one, and reading only the outer one is worse than incomplete. Pairing is injective, so a one-layer reader silently matches the arity against the constructor tag and binds the payload's own tag as though it were a subcode: the clause is then vacuous at every arity but one, and wrong at that one. Nothing in Agda reports this, because the reader is still true; it simply cannot be supplied.

Both layers are read by one existential over the inner code, with the pair reader above pinning the outer layer and the tag reader the inner. The arity is left as a variable, so a clause can speak of it, which the four constructors that change arity need.

arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b =
  ∃̇ (prAtL (suc c) (suc ar) zero ∧̇ tagPairAtL zero k (suc a) (suc b))

arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ))
        (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ)))))
arityTagPairAtL-adequate c ar k a b γ = ⇔toPath fwd bwd
  where
  N = fst (lookup ar γ)
  P = pr (fst (lookup a γ)) (fst (lookup b γ))
  target = PairIs (fst (lookup c γ)) (pr N (pr (# k) P))

  fwd : ⟨ γ ⊨ arityTagPairAtL c ar k a b ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , t)) →
      subst ⟨_⟩ (prAtL-adequate (suc c) (suc ar) zero (z ∷ γ)) p
      ∙ cong (pr N) (subst ⟨_⟩ (tagPairAtL-adequate zero k (suc a) (suc b) (z ∷ γ)) t) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ arityTagPairAtL c ar k a b ⟩
  bwd q = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate (suc c) (suc ar) zero (zS ∷ γ)))
          (q ∙ cong (pr N) (sym e))
      , subst ⟨_⟩ (sym (tagPairAtL-adequate zero k (suc a) (suc b) (zS ∷ γ))) e ) ∣₁
    where
    zS : S
    zS = prʟ (numeralL k) (prʟ (lookup a γ) (lookup b γ))
    e : fst zS ≡ pr (# k) P
    e = prʟ-fst (numeralL k) (prʟ (lookup a γ) (lookup b γ))
      ∙ cong₂ pr (numeralL-fst k) (prʟ-fst (lookup a γ) (lookup b γ))

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n
arityTagAtL c ar k a =
  ∃̇ (prAtL (suc c) (suc ar) zero ∧̇ tagAtL zero k (suc a))

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagAtL c ar k a)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ)) (pr (# k) (fst (lookup a γ))))
arityTagAtL-adequate c ar k a γ = ⇔toPath fwd bwd
  where
  N = fst (lookup ar γ)
  A = fst (lookup a γ)
  target = PairIs (fst (lookup c γ)) (pr N (pr (# k) A))

  fwd : ⟨ γ ⊨ arityTagAtL c ar k a ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , t)) →
      subst ⟨_⟩ (prAtL-adequate (suc c) (suc ar) zero (z ∷ γ)) p
      ∙ cong (pr N) (subst ⟨_⟩ (tagAtL-adequate zero k (suc a) (z ∷ γ)) t) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ arityTagAtL c ar k a ⟩
  bwd q = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate (suc c) (suc ar) zero (zS ∷ γ)))
          (q ∙ cong (pr N) (sym e))
      , subst ⟨_⟩ (sym (tagAtL-adequate zero k (suc a) (zS ∷ γ))) e ) ∣₁
    where
    zS : S
    zS = prʟ (numeralL k) (lookup a γ)
    e : fst zS ≡ pr (# k) A
    e = prʟ-fst (numeralL k) (lookup a γ) ∙ cong₂ pr (numeralL-fst k) refl

Looking a subcode up in the table

The frames bind a code's payload but never look the table up at it, because a payload component may be a term code, at which the table has nothing. A relation that does want the value must therefore build the key itself: pair the arity with the component, and read the table there.

That is one existential over the key, and it is the piece four of the twelve relations are built from. The two that speak of a subformula at the next arity need the same thing with the arity bumped, which is this with one more layer.

subValAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
subValAt T ar a y =
  ∃̇ (prAtL zero (suc ar) (suc a) ∧̇ appAt (suc T) zero (suc y))

subValAt-adequate : ∀ {n} (T ar a y : Fin n) (γ : S ^ n)
  → (γ ⊨ subValAt T ar a y)
  ≡ (pr (pr (fst (lookup ar γ)) (fst (lookup a γ))) (fst (lookup y γ))
      ∈ fst (lookup T γ))
subValAt-adequate T ar a y γ = ⇔toPath fwd bwd
  where
  K = pr (fst (lookup ar γ)) (fst (lookup a γ))
  target = pr K (fst (lookup y γ)) ∈ fst (lookup T γ)

  fwd : ⟨ γ ⊨ subValAt T ar a y ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , q)) →
      subst (λ w → ⟨ pr w (fst (lookup y γ)) ∈ fst (lookup T γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc ar) (suc a) (z ∷ γ)) p)
        (subst ⟨_⟩ (appAt-adequate (suc T) zero (suc y) (z ∷ γ)) q) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ subValAt T ar a y ⟩
  bwd h = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc ar) (suc a) (zS ∷ γ))) e
      , subst ⟨_⟩ (sym (appAt-adequate (suc T) zero (suc y) (zS ∷ γ)))
          (subst (λ w → ⟨ pr w (fst (lookup y γ)) ∈ fst (lookup T γ) ⟩) (sym e) h) ) ∣₁
    where
    zS : S
    zS = prʟ (lookup ar γ) (lookup a γ)
    e : fst zS ≡ K
    e = prʟ-fst (lookup ar γ) (lookup a γ)

The shape of a clause

A recursion on codes is stated by clauses, and the clauses come in a few shapes rather than twelve. A binary constructor's clause says: for every code in the index with this tag over these two subcodes, and for the values the table records at the three of them, such-and-such holds. All of that is fixed except the such-and-such, so it is written once with the relation as a parameter, and the three binary constructors differ only in which relation they hand it.

Five things are bound, in the order a reader meets them: the code, its arity, its two payload components, and the value the table records at the code. The values at the payload components are not bound, and that is what makes the frame general. A connective's payload is a pair of formula codes and its clause does want them, but an atom's payload is a pair of term codes, at which the table has no entries at all, and a bounded quantifier's payload mixes the two. So the frame binds what every constructor has and leaves the lookups to the relation, which may perform them freely.

Reading the clause back is one chain of substitutions along the readers' adequacy, and it is stated in the direction a soundness proof consumes: given a code of that shape in the index and the three recorded values, the relation holds.

module _ {n : ℕ} where
  private
    sh5 : Fin n → Fin ( + n)
    sh5 i = suc (suc (suc (suc (suc i))))

    c5 n5 a5 b5 yc5 : Fin ( + n)
    c5  = suc (suc (suc (suc zero)))
    n5  = suc (suc (suc zero))
    a5  = suc (suc zero)
    b5  = suc zero
    yc5 = zero

  binClauseAt : Fin n → Fin n → ℕ → Formula S ( + n) → Formula S n
  binClauseAt C T k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ (∀̇ (∀̇
      ( arityTagPairAtL c5 n5 k a5 b5
      ⇒̇ ( appAt (sh5 T) c5 yc5
      ⇒̇ rel ))))))

  binClause-out : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ binClauseAt C T k rel ⟩
    → (c ar a b yc : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
    → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
    → ⟨ (yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
  binClause-out C T k rel γ h c ar a b yc c∈ shape hc =
    h c c∈ ar a b yc
      (subst ⟨_⟩ (sym (arityTagPairAtL-adequate c5 n5 k a5 b5 δ)) shape)
      (subst ⟨_⟩ (sym (appAt-adequate (sh5 T) c5 yc5 δ)) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ b ∷ a ∷ ar ∷ c ∷ γ

Each frame reads the other way too, and the other way is what an instance uses. The elimination takes a clause apart for a consumer who has a code in hand; the introduction assembles one for a table that has to satisfy it. Both frames introduce by a lambda, because a bounded universal over the model is a function on members and an implication is a function on the reader's proof, so the two are the same substitutions run backwards.

  binClause-in : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a b yc : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
       → ⟨ (yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
    → ⟨ γ ⊨ binClauseAt C T k rel ⟩
  binClause-in C T k rel γ g c c∈ ar a b yc sh hc =
    g c ar a b yc c∈
      (subst ⟨_⟩ (arityTagPairAtL-adequate c5 n5 k a5 b5 δ) sh)
      (subst ⟨_⟩ (appAt-adequate (sh5 T) c5 yc5 δ) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ b ∷ a ∷ ar ∷ c ∷ γ

Counting the shapes is worth a moment, because it says how much of the twelve is really there, and because counting it wrong is easy: this paragraph has been wrong twice.

The frames distinguish exactly one thing, whether the payload is a pair or a single component. The pair frame covers the two atoms, the three connectives and the two bounded quantifiers, which is seven; the single-component frame covers negation, the two unbounded quantifiers, and the two constants, which is five, since a constant's payload is a numeral and the frame does not care what a component is. Two frames, then, and twelve relations above them.

What the frames must not distinguish is what the payload components are. Grouping by that gives five kinds of relation, not five frames: term against term, formula against formula, term against formula, one formula, and one formula at the next arity. That is where the twelve actually divide, and it divides them in the relations, where the lookups live.

The single-component frame is the pair frame with one binder fewer, and reads back the same way.

  private
    sh4 : Fin n → Fin ( + n)
    sh4 i = suc (suc (suc (suc i)))

    c4 n4 a4 yc4 : Fin ( + n)
    c4  = suc (suc (suc zero))
    n4  = suc (suc zero)
    a4  = suc zero
    yc4 = zero

  unClauseAt : Fin n → Fin n → ℕ → Formula S ( + n) → Formula S n
  unClauseAt C T k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ (∀̇
      ( arityTagAtL c4 n4 k a4
      ⇒̇ ( appAt (sh4 T) c4 yc4
      ⇒̇ rel )))))

  unClause-out : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ unClauseAt C T k rel ⟩
    → (c ar a yc : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
    → ⟨ (yc ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
  unClause-out C T k rel γ h c ar a yc c∈ shape hc =
    h c c∈ ar a yc
      (subst ⟨_⟩ (sym (arityTagAtL-adequate c4 n4 k a4 δ)) shape)
      (subst ⟨_⟩ (sym (appAt-adequate (sh4 T) c4 yc4 δ)) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ a ∷ ar ∷ c ∷ γ

  unClause-in : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a yc : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))
       → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
       → ⟨ (yc ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
    → ⟨ γ ⊨ unClauseAt C T k rel ⟩
  unClause-in C T k rel γ g c c∈ ar a yc sh hc =
    g c ar a yc c∈
      (subst ⟨_⟩ (arityTagAtL-adequate c4 n4 k a4 δ) sh)
      (subst ⟨_⟩ (appAt-adequate (sh4 T) c4 yc4 δ) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ a ∷ ar ∷ c ∷ γ

The positive connectives

Two of the twelve can be written now, and they are the two that need nothing the chapter has not got. Conjunction and disjunction relate the value at a code to the values at its two subcodes by intersection and union, at the same arity, and that is the whole of their content.

The shared part is a relation that binds the two subvalues and guards them with the table lookups; the operation is what is left over, and it speaks of the value at the code and the two subvalues, at positions two, one and zero. So a propositional clause is one line above the shared part.

Implication and negation want the complement, hence the set of all environments at the code's arity, which the chapter does not yet name. They wait for it. The split is not arbitrary: it is exactly the split between the connectives whose truth is monotone in their parts and those whose truth is not.

module _ {n : ℕ} where
  private
    sh7 : Fin n → Fin ( + n)
    sh7 i = suc (suc (suc (suc (suc (suc (suc i))))))

  c7 ar7 a7 b7 yc7 ya7 yb7 : Fin ( + n)
  c7  = suc (suc (suc (suc (suc (suc zero)))))
  ar7 = suc (suc (suc (suc (suc zero))))
  a7  = suc (suc (suc (suc zero)))
  b7  = suc (suc (suc zero))
  yc7 = suc (suc zero)
  ya7 = suc zero
  yb7 = zero

  propRel : Fin n → Formula S ( + n) → Formula S ( + n)
  propRel T op =
    ∀̇ (∀̇ ( subValAt (sh7 T) ar7 a7 ya7
         ⇒̇ ( subValAt (sh7 T) ar7 b7 yb7
         ⇒̇ op )))

  propClauseAt : Fin n → Fin n → ℕ → Formula S ( + n) → Formula S n
  propClauseAt C T k op = binClauseAt C T k (propRel T op)

  propClause-out : (C T : Fin n) (k : ℕ) (op : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ propClauseAt C T k op ⟩
    → (c ar a b yc ya yb : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
    → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
    → ⟨ pr (pr (fst ar) (fst a)) (fst ya) ∈ fst (lookup T γ) ⟩
    → ⟨ pr (pr (fst ar) (fst b)) (fst yb) ∈ fst (lookup T γ) ⟩
    → ⟨ (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ op ⟩
  propClause-out C T k op γ h c ar a b yc ya yb c∈ shape hc ha hb =
    binClause-out C T k (propRel T op) γ h c ar a b yc c∈ shape hc ya yb
      (subst ⟨_⟩ (sym (subValAt-adequate (sh7 T) ar7 a7 ya7 δ)) ha)
      (subst ⟨_⟩ (sym (subValAt-adequate (sh7 T) ar7 b7 yb7 δ)) hb)
    where
    δ : S ^ ( + n)
    δ = yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ

  propClause-in : (C T : Fin n) (k : ℕ) (op : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a b yc ya yb : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
       → ⟨ pr (pr (fst ar) (fst a)) (fst ya) ∈ fst (lookup T γ) ⟩
       → ⟨ pr (pr (fst ar) (fst b)) (fst yb) ∈ fst (lookup T γ) ⟩
       → ⟨ (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ op ⟩)
    → ⟨ γ ⊨ propClauseAt C T k op ⟩
  propClause-in C T k op γ g =
    binClause-in C T k (propRel T op) γ
      (λ c ar a b yc c∈ sh hc ya yb ha hb →
        g c ar a b yc ya yb c∈ sh hc
          (subst ⟨_⟩
            (subValAt-adequate (sh7 T) ar7 a7 ya7 (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ)) ha)
          (subst ⟨_⟩
            (subValAt-adequate (sh7 T) ar7 b7 yb7 (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ)) hb))

  andClauseAt : Fin n → Fin n → Formula S n
  andClauseAt C T = propClauseAt C T  (interAt yc7 ya7 yb7)

  orClauseAt : Fin n → Fin n → Formula S n
  orClauseAt C T = propClauseAt C T  (unionAt yc7 ya7 yb7)