The order, described in the object language

The previous chapters built the order this part turns on, and built all of it in the meta-language: a family of well-orders, one at every ordinal, comparing two sets by their births and, at a common birth, by their least names. None of that is speakable inside L. What the argument ahead needs is a formula: the same comparison described in the object language, so that the model's own separation can carve the order out as a set and the choosing can be written down inside.

This chapter writes that description. It has three parts, and each is the reading of one meta-level part. A name at slots says what a skeleton, a parameter sequence and a denotation are; the order formula compares two names by the three keys the naming chapter compared them by; and the step says what one step of the family does. The chapter closes with the two halves that make a description a description: at a variable environment, the order formula holds of two names' data exactly when the naming chapter's comparison holds of the names.

Two decisions shape everything below. The two conditions that say a formula is a skeleton are each one membership atom, one in the limit stage and one in the code set at the empty alphabet, and neither is a recursion; and the order formula runs no recursion of its own. Both are explained where they are used, because both are the reason this chapter is short.

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

open import Base.Prelude
open import Base.Truth
open import Base.Classical using ( LEM )

module L.Choice.Internal {ℓ : 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 FOL.Manipulation.Relabelling using ( mapFo; mapFo-comp; embed )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL; isL-trans; Lset )
open import L.Ordinal {ℓ} using ( ω-ord; ∈#-elim; #∈#-elim )
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.Model {ℓ}
  using ( extAt; extAt-out; extAt-in-both
        ; prAtL; prAtL-adequate; appAt; appAt-adequate
        ; domAt; domAt-in; domAt-out; domAt-intro; numL
        ; sucAtL; sucAtL-adequate; envOverAt; consAtL )
open import L.Coding.Sat {ℓ} lem using ( Sat )
open import L.Coding.Table {ℓ} lem
  using ( slot; satTable; total; inSlot; entry-in )
open import L.Coding.Slot {ℓ} lem using ( slotClosed )
open import L.Coding.Sound {ℓ} lem using ( soundness )
open import L.Coding.Unique {ℓ} lem using ( module Good )
open import L.Coding.Bridge {ℓ} lem using ( asConst )
open import L.Coding.CodeSet {ℓ} lem
  using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Coding.Uniform {ℓ} lem using ( keyBridge )
open import L.Coding.Graph {ℓ} lem using ( satGraphAt; graphAt-in; graphAt-out )
open import L.Coding.Sequence {ℓ} lem using ( LsetGraphAt )
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Choice.Name {ℓ} lem using ( module Naming; limitCode; code∈limit )
open import L.Choice.Finite {ℓ} lem using ( Limit; limitOrder )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )

open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2; J; substRefl )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; 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
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

  sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n)))))
  sh5 i = suc (suc (suc (suc (suc i))))

A skeleton, said as one atom

A name's formula carries no parameters: the parameters left the syntax two chapters ago and arrived as an environment. Saying so inside the model looks, at first, like a demand for a recursion. "No constant tag occurs anywhere in this code" is a statement about every subcode, and a statement about every subcode is a descent, which would have to be internalized with its own graph, its own table and its own uniqueness theorem.

The descent is not needed, and this is the chapter's cheapest line. A parameter-free code is built from numerals and Kuratowski pairs and from nothing else, so it is hereditarily finite, and the naming chapter proved exactly that: the code lies in Lset ω. Membership is one atom. So the first condition the description carries is that the skeleton belongs to the limit stage, and the sequence chapter already says inside what the limit stage is, as the value its graph assigns at the constant ωʟ. What that atom does not say is constant-freeness itself, and the next section says it, with a second atom rather than a recursion.

The graph is discharged at a variable pair of slots reached by two equations, which is the law the tower chapters were written under, and the two elements the description is satisfied at are sealed for the reason the marker records.

-- perf: the limit stage's two elements are sealed; unsealed, checking any term
-- at a satisfaction of the tower graph over them runs 77 s instead of 1.6 s
opaque
  ωAt : S
  ωAt = ωʟ

  ωStage : S
  ωStage = LsetS ω ω-ord

  ωAt-fst : fst ωAt ≡ ω
  ωAt-fst = refl

  ωStage-fst : fst ωStage ≡ Lset ω
  ωStage-fst = refl

limitGraph : ∀ {n} (v o : Fin n) (γ : S ^ n)
           → fst (lookup o γ) ≡ ω → fst (lookup v γ) ≡ Lset ω
           → ⟨ γ ⊨ LsetGraphAt v o ⟩
limitGraph v o γ qo qv =
  Lset-defines v o γ (subst IsOrd (sym qo) ω-ord) (qv ∙ cong Lset (sym qo))

InLimitAt : ∀ {n} → Fin n → Formula S n
InLimitAt s = ∃̇ (∃̇ ( (var zero ≐ con ωʟ)
                    ∧̇ ( LsetGraphAt (suc zero) zero
                      ∧̇ (var (sh2 s) ∈̇ var (suc zero)) ) ))

module _ {n : ℕ} (s : Fin n) (γ : S ^ n) where
  private
    Held : S → Type (ℓ-suc ℓ)
    Held v = Σ[ o ∈ S ] ( (fst o ≡ ω)
                        × ( ⟨ (o ∷ v ∷ γ) ⊨ LsetGraphAt (suc zero) zero ⟩
                          × ⟨ fst (lookup s γ) ∈ fst v ⟩ ) )

  InLimitAt-in : ⟨ fst (lookup s γ) ∈ Lset ω ⟩ → ⟨ γ ⊨ InLimitAt s ⟩
  InLimitAt-in h = ∣ ωStage , ∣ ωAt , (ωAt-fst , (gr , held)) ∣₁ ∣₁
    where
    gr : ⟨ (ωAt ∷ ωStage ∷ γ) ⊨ LsetGraphAt (suc zero) zero ⟩
    gr = limitGraph (suc zero) zero (ωAt ∷ ωStage ∷ γ) ωAt-fst ωStage-fst
    held : ⟨ fst (lookup s γ) ∈ fst ωStage ⟩
    held = subst (λ u → ⟨ fst (lookup s γ) ∈ u ⟩) (sym ωStage-fst) h

  InLimitAt-out : ⟨ γ ⊨ InLimitAt s ⟩ → ⟨ fst (lookup s γ) ∈ Lset ω ⟩
  InLimitAt-out = PT.rec (snd (fst (lookup s γ) ∈ Lset ω)) atValue
    where
    read : (v : S) → Held v → ⟨ fst (lookup s γ) ∈ Lset ω ⟩
    read v (o , (qo , (hg , hs))) =
      subst (λ u → ⟨ fst (lookup s γ) ∈ u ⟩)
        (Lset-only (suc zero) zero (o ∷ v ∷ γ) hg oo ∙ cong Lset qo) hs
      where
      oo : IsOrd (fst o)
      oo = subst IsOrd (sym qo) ω-ord

    atValue : Σ[ v ∈ S ] ∥ Held v ∥₁ → ⟨ fst (lookup s γ) ∈ Lset ω ⟩
    atValue (v , hv) = PT.rec (snd (fst (lookup s γ) ∈ Lset ω)) (read v) hv

The same code at the empty alphabet

That condition puts the code where the order of codes lives, and it is not the condition the meta-language imposes. A member of the limit stage is a hereditarily finite set, and a hereditarily finite set can be the code of a formula whose constants are hereditarily finite; over a carrier containing the limit stage those constants are members of the carrier, so the skeleton condition alone admits skeletons the meta Name excludes, and a least name inside would not have to be a least name outside. The description has to say the other thing as well: the skeleton carries no constants.

It costs one more membership atom, and it reuses a set the coding chapters already build. AllCodes A holds exactly the keys of the formulas over the alphabet ⟪ A ⟫; take the alphabet empty and it holds exactly the keys of the parameter-free formulas. So the second code set reaches the description as a slot, like the first, and the atom says that the key made from the arity and the skeleton lies in it.

One thing had to be checked before writing that down, and it holds: a parameter-free formula has the same code at either alphabet. Both readings of its constants are functions out of an empty type, any two such agree, and relabelling composes, so the two codes are the same set, four lines in each direction. Nothing has to be satisfied at the empty alphabet, because the conjunct is an atom and the separation the code set was cut out by was proved generic in its carrier where it was built.

The bridge is then the code set's own two directions read at that alphabet, with the arity moved along the equality of numerals by path induction, once, in the direction that leaves the code alone.

private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)

  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫

  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = Empty.rec (noAlpha m)

  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m)))
             ∙ sym (mapFo-comp ε Empty.rec* ψ)

  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))

  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift {i} e ψ =
    J (λ j' e' → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e' ψ) ⌝
               ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝)
      (cong (λ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) (substRefl {B = Fo∅} ψ)) e

freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))

freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩
             → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁
freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩
  cL = isL-trans h (AllCodes ∅ʟ .snd)

  read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ))
       → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ))
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k
    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')

Constant-freeness, said as one atom

The atom itself binds two values before it can be stated. The arity slot holds the name's arity, and the key a formula is filed under carries one more, because the formula is the one a subset is carved by; so the atom binds the successor of the arity, which the sequence chapter's reader already says, then the pair of that successor with the skeleton, and then asserts that pair to be a member of the second code set.

Both readings are at a variable arity reached by an equation, and both are the binders packed and unpacked with the two readers' adequacy equations discharged inside. With the slot filled, the two halves compose into the statement the gap asked for: the skeleton slot holds exactly the codes of the parameter-free formulas of one more variable than the arity, which is exactly what a meta name's formula is. The membership in the limit stage falls out of it for free, since a parameter-free code is hereditarily finite, so the skeleton condition of the previous section is now derivable rather than assumed;

codeFree-limit is that warrant, and the description keeps both conjuncts until the derivable one is retired on purpose.

FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )

module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) where

  FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
    where
    numAt : S
    numAt = # (suc k) , numL (suc k)
    keyAt : S
    keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd)
    hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
    hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
      (cong sucV (sym qa))
    hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
    hpr = subst ⟨_⟩
      (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl

  FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
  FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                            ∈ fst (lookup C₀ γ))) atNum
    where
    Target : Type (ℓ-suc ℓ)
    Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩

    atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ))
          → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                       × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ )
          → Target
    atKey z qz (y , (hp , hy)) =
      subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
         ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy

    atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                       × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                       ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
          → Target
    atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                                         ∈ fst (lookup C₀ γ)))
      (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk

module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ))
         (qa : fst (lookup a γ) ≡ # k) where

  codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
               → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                     (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁
  codeFree-out h = freeCode-out (suc k) (fst (lookup s γ))
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀
      (FreeAt-out C₀ s a γ k qa h))

  codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
              → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  codeFree-in χ q = FreeAt-in C₀ s a γ k qa
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀)
      (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)
        (freeCode-in (suc k) χ)))

  codeFree-limit : ⟨ γ ⊨ FreeAt C₀ s a ⟩ → ⟨ fst (lookup s γ) ∈ Lset ω ⟩
  codeFree-limit h =
    PT.rec (snd (fst (lookup s γ) ∈ Lset ω)) atCode (codeFree-out h)
    where
    atCode : Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
               (fst (lookup s γ) ≡ fst (limitCode χ))
           → ⟨ fst (lookup s γ) ∈ Lset ω ⟩
    atCode (χ , q) = subst (λ u → ⟨ u ∈ Lset ω ⟩) (sym q) (code∈limit χ)

How long a sequence is

The parameter sequence is a function, and how long it is is what its domain says. One fact is wanted, in both directions, and it is used twice below: the domain of an environment of length k is the numeral of k. Forwards, an entry is a pair whose first component is the numeral of an index, and an index is smaller than the length. Backwards, a member of the numeral is the numeral of a smaller number, that number is an index, and the environment has an entry there.

The statement stands at a variable environment reached by an equation saying which family it is the graph of, and the family's values are supplied with their constructibility, because an object-language function must hand back an element of the model when it is applied.

private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = PT.map
    (λ { (li , e) → lower li
       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })

  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁

  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ⋁ S (λ y → pr x (fst y) ∈ env g) ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))
            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))
      (memberOf k g x (fst y) p)

  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ⋁ S (λ y → pr x (fst y) ∈ env g) ⟩
  dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))
              → Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k
      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))

module _ {n : ℕ} (e d : Fin n) (γ : S ^ n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : fst (lookup e γ) ≡ env g) where

  domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k
  domAt-numeral h = extensionalV {a = fst (lookup d γ)} {b = # k} pt
    where
    fwd : (x : V ℓ) → ⟨ x ∈ fst (lookup d γ) ⟩ → ⟨ x ∈ # k ⟩
    fwd x hx = dom-into k g x
      (subst (λ u → ⟨ ⋁ S (λ y → pr x (fst y) ∈ u) ⟩) qe
        (domAt-in e d γ h (x , isL-trans hx (lookup d γ .snd)) hx))
    bwd : (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ x ∈ fst (lookup d γ) ⟩
    bwd x hx = PT.rec (snd (x ∈ fst (lookup d γ))) put (dom-from k g cg x hx)
      where
      xS : S
      xS = x , isL-trans hx (numL k)
      put : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ fst (lookup d γ) ⟩
      put (y , p) = domAt-out e d γ h xS y
        (subst (λ u → ⟨ pr x (fst y) ∈ u ⟩) (sym qe) p)
    pt : (x : V ℓ) → (x ∈ fst (lookup d γ)) ≡ (x ∈ # k)
    pt x = ⇔toPath (fwd x) (bwd x)

  domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩
  domAt-fill qd = domAt-intro e d γ step
    where
    step : (x : S)
         → (⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ fst (lookup e γ)) ⟩
            → ⟨ fst x ∈ fst (lookup d γ) ⟩)
         × (⟨ fst x ∈ fst (lookup d γ) ⟩
            → ⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ fst (lookup e γ)) ⟩)
    step x =
        (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)
          (subst (λ u → ⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ u) ⟩) qe hy)))
      , (λ hx → subst (λ u → ⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ u) ⟩) (sym qe)
          (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))

What the satisfaction graph assigns

The denotation is what a name's formula selects, and inside the model the selecting is done by the satisfaction table. The uniform-satisfaction chapter built that table as a recursion and proved its two halves against the model's own two-place graph. What is needed here is the same two halves at a carrier held in a slot and at a variable ambient environment, because the description below puts the graph under five binders.

Nothing is re-proved. The index set, the table, its closedness, its totality and the twelve clauses are the chapters that built them, applied at this environment; the key is carried from the hierarchy's coding to the model's by the bridge written for exactly that. So the two readings are the existence and the uniqueness halves transplanted, and they say what a consumer wants: the value the graph assigns at the key of a formula is that formula's satisfaction set, and nothing else satisfies the graph there.

module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where
  private
    Ci Ti : Fin (suc (suc (suc n)))
    Ci = suc (suc zero)
    Ti = suc zero

    Bs : S
    Bs = lookup B γ

    δ : ∀ {m} (φ : Formula S m) → S ^ (suc (suc (suc n)))
    δ φ = Bs ∷ satTable Bs φ ∷ slot Bs φ ∷ γ

    hdom : ∀ {m} (φ : Formula S m) → ⟨ δ φ ⊨ domAt Ti Ci ⟩
    hdom φ = domAt-intro Ti Ci (δ φ)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ)))
                 (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h)
           , (λ h → total Bs φ (fst z) h))

  graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
                → fst (lookup x γ) ≡ fst (keyS Bs ψ)
                → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
                → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-value ψ qx qy = graphAt-in B x y γ
    ∣ slot Bs φ , (satTable Bs φ , (Bs , (refl
    , ( slotClosed Bs φ γ
    , ( hdom φ
    , ( subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩)
          (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
    , soundness Bs φ γ )))))) ∣₁
    where
    φ : Formula S _
    φ = mapFo (asConst Bs) ψ

  graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
               → fst (lookup x γ) ≡ fst (keyS Bs ψ)
               → ⟨ γ ⊨ satGraphAt B x y ⟩
               → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
  graphAt-only ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)
    where
    φ : Formula S _
    φ = mapFo (asConst Bs) ψ

    read : _ → fst (lookup y γ) ≡ fst (Sat Bs φ)
    read (C , (T , (b , (eb , (hc , (hd , (ha , h12))))))) =
        Good.pinned (b ∷ T ∷ C ∷ γ) Ci Ti zero hc hd h12 φ
          (lookup x γ) (lookup y γ) (qx ∙ keyBridge Bs ψ)
          (domAt-out Ti Ci (b ∷ T ∷ C ∷ γ) hd (lookup x γ) (lookup y γ) ha) ha
      ∙ cong (λ w → fst (Sat w φ)) (Σ≡Prop (λ v → snd (isL v)) eb)

A name, described at slots

A name is three things, and the description carries them at three slots: the skeleton, the code of the parameter-free formula; the parameter sequence, an environment over the carrier; and the denotation, the set the name names. A fourth slot holds the arity, which is not a fourth part but the sequence's own domain, pinned by the same conjunct that says the sequence is an environment over the carrier.

The denotation is the one conjunct with mathematics in it, and it is written as one extension, for the reason every set-valued clause on this route is: a value is the set of exactly the things meeting a condition, and writing that as a pair of inclusions would say the condition twice. A member of the carrier belongs to the denotation exactly when the environment got by pushing that member onto the parameters satisfies the skeleton, and satisfying is read off the value the graph assigns. So the body binds, in order, the extended environment, its length, the key that length and the skeleton make, and the value at that key.

One conjunct is easy to miss and the description says nothing without it: the key must lie in the code set. The graph binds its table existentially, so at a key that is nobody's code a table may record anything at all; the code set is what makes the value determinate, and it reaches the description as a slot, like the carrier.

Both readings are the extension's own two directions with the four binders packed and unpacked, and every payload is named. The key equation is handed back decoded, because a consumer wants the equation and not the syntax that carries it.

DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero
            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )

NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  InLimitAt s ∧̇ ( FreeAt C₀ s a
                ∧̇ ( (var a ∈̇ con ωʟ)
                  ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) ) )

module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where
  AtValue : (z c k key : S) → Type (ℓ-suc ℓ)
  AtValue z c k key = Σ[ v ∈ S ]
    ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
    × ⟨ fst c ∈ fst v ⟩ )

  AtKey : (z c k : S) → Type (ℓ-suc ℓ)
  AtKey z c k = Σ[ key ∈ S ]
    ( ⟨ fst key ∈ fst (lookup C γ) ⟩
    × ( ⟨ (key ∷ k ∷ c ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh4 s) ⟩
      × ∥ AtValue z c k key ∥₁ ) )

  AtArity : (z c : S) → Type (ℓ-suc ℓ)
  AtArity z c = Σ[ k ∈ S ]
    ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩ × ∥ AtKey z c k ∥₁ )

  AtCons : (z : S) → Type (ℓ-suc ℓ)
  AtCons z = Σ[ c ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩ × ∥ AtArity z c ∥₁ )

  DenoteOf : (z : S) → Type (ℓ-suc ℓ)
  DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
      × ( ⟨ fst key ∈ fst (lookup C γ) ⟩
        × ( (fst key ≡ pr (fst k) (fst (lookup s γ)))
          × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
            × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )

  DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z
                → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
  DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp
      , ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁

  DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
                 → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁
  DenoteBody-out z (hz , hc) = hz , PT.rec squash₁ (atCons z) hc
    where
    atValue : (z c k key : S) → ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
            → ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
            → ⟨ fst key ∈ fst (lookup C γ) ⟩
            → ⟨ (key ∷ k ∷ c ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh4 s) ⟩
            → AtValue z c k key → ∥ DenoteOf z ∥₁
    atValue z c k key hc hk hi hp (v , (hg , hm)) =
      ∣ c , (k , (key , (v , (hc , (hk , (hi
      , ( subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp
        , (hg , hm) ))))))) ∣₁

    atKey : (z c k : S) → ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
          → ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
          → AtKey z c k → ∥ DenoteOf z ∥₁
    atKey z c k hc hk (key , (hi , (hp , hv))) =
      PT.rec squash₁ (atValue z c k key hc hk hi hp) hv

    atArity : (z c : S) → ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
            → AtArity z c → ∥ DenoteOf z ∥₁
    atArity z c hc (k , (hk , hkey)) =
      PT.rec squash₁ (atKey z c k hc hk) hkey

    atCons : (z : S) → AtCons z → ∥ DenoteOf z ∥₁
    atCons z (c , (hc , ha)) = PT.rec squash₁ (atArity z c hc) ha

module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where
  NameAt-in : ⟨ fst (lookup s γ) ∈ Lset ω ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
            → ⟨ fst (lookup a γ) ∈ ω ⟩
            → ⟨ γ ⊨ envOverAt e a B ⟩
            → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
               → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z)
            → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
               → ⟨ fst z ∈ fst (lookup d γ) ⟩)
            → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
  NameAt-in hs hf ha he into back =
    InLimitAt-in s γ hs , (hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ
      (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd))
      (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ)))
                 (back z (DenoteBody-out B C s e γ z h .fst))
                 (DenoteBody-out B C s e γ z h .snd)))))

  NameAt-out : ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
             → ⟨ fst (lookup s γ) ∈ Lset ω ⟩
             × ( ⟨ γ ⊨ FreeAt C₀ s a ⟩
               × ( ⟨ fst (lookup a γ) ∈ ω ⟩
                 × ( ⟨ γ ⊨ envOverAt e a B ⟩
                   × ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
                      → ⟨ fst z ∈ fst (lookup B γ) ⟩
                      × ∥ DenoteOf B C s e γ z ∥₁) ) ) )
  NameAt-out (hl , (hf , (ha , (he , hd)))) =
    InLimitAt-out s γ hl , (hf , (ha , (he
    , λ z hz → DenoteBody-out B C s e γ z
                 (extAt-out d (DenoteBody B C s e) γ hd z hz))))

The order, with no recursion of its own

The naming chapter compared two names by three keys: the code, by the well-order of the limit stage; the arity, by the order of the numerals; and the parameters, at the first place they differ. Every one of the three is available inside without a recursion, and that is the fact worth stating plainly, because a second internalized recursion is the largest cost this route has ever paid.

The first key is a membership atom. The order the codes are compared by is a relation, a relation is a set of pairs, and "this code comes before that one" is "the pair of them belongs to that set". The relation reaches the description as a slot: the description is a frame, and what fills the slot is the caller's business, which is also why nothing here has to know how that order was built.

The second key is a membership atom as well, because an arity is a numeral and a numeral is the set of the smaller numerals.

The third key is a bounded quantification, not a descent. Two sequences of the same length differ first somewhere, and below that index they agree. Written out, that is one bounded existential over the index, two applications reading the two values there, one membership atom against the parameter order, and one bounded universal saying the two sequences agree below. Nothing recurses, nothing is defined by cases on a code, and no second table is wanted.

private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))

  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = suc (suc (suc (suc (suc (suc i)))))

LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
LexAt P a e₁ e₂ =
  ∃̇∈ (var a) (
    ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero)
           ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero
             ∧̇ ( appAt (sh3 P) (suc zero) zero
               ∧̇ ∀̇∈ (var (suc (suc zero))) (
                    ∃̇ ( appAt (sh5 e₁) (suc zero) zero
                      ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )

≺At : ∀ {n} → Fin n → Fin n
    → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n
≺At R P s₁ a₁ e₁ s₂ a₂ e₂ =
      appAt R s₁ s₂
  ∨̇ ( (var s₂ ≐ var s₁)
    ∧̇ ( (var a₁ ∈̇ var a₂)
      ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )

module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where
  private
    Body : Formula S (suc (suc (suc (suc (suc n)))))
    Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero

    Inner : (i u v : S) → Type (ℓ-suc ℓ)
    Inner i u v =
      ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩
      × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩
        × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩
          × ((j : S) → ⟨ fst j ∈ fst i ⟩
             → ⟨ ⋁ S (λ x → (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body) ⟩) ) )

  Agrees : (i : S) → Type (ℓ-suc ℓ)
  Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩
           → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                          × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁

  Differs : Type (ℓ-suc ℓ)
  Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ]
    ( ⟨ fst i ∈ fst (lookup a γ) ⟩
    × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩
      × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩
        × ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )

  private
    pack : (i u v : S) → Inner i u v → Agrees i
    pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩
               (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁
           , subst ⟨_⟩
               (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) })
      (hj j hj')

    unpack : (i u v : S) → Agrees i
           → (j : S) → ⟨ fst j ∈ fst i ⟩
           → ⟨ ⋁ S (λ x → (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body) ⟩
    unpack i u v hj j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁
           , subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) })
      (hj j hj')

  LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩
  LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj)))))))
    = ∣ i , (hi , ∣ u , ∣ v
    , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁
      , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂
        , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp
          , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁
    where
    γ₃ : S ^ (suc (suc (suc n)))
    γ₃ = v ∷ u ∷ i ∷ γ

  LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁
  LexAt-out = PT.rec squash₁ atIndex
    where
    atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs
    atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v
      , ( hi
        , ( subst ⟨_⟩
              (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁
          , ( subst ⟨_⟩
                (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂
            , ( subst ⟨_⟩
                  (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp
              , pack i u v h ) ) ) ) ))

    atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
             → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁
    atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁

    atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
            → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁
    atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h

    atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩
                         × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ )
            → ∥ Differs ∥₁
    atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h

Reading the comparison, and one step of the family

The comparison's reading is its three cases sorted. The object language's disjunctions are truncated, so the elimination lands in a truncation and the introduction does not, and the payload is written out rather than inferred.

The step is the family's own step, described. One member of the new stage comes before another when the least name of the first comes before the least name of the second, and "least" is said the way it is always said: this is a name of that set, and no name of that set comes before it. The meta step has one branch since the surplus one was deleted, so this description has one too; the min-difference formula the plan once wanted to guard a second branch with is not written, because there is no second branch.

Six binders carry the two names, and they are a frame generic in the body under them. Read directly, packing or unpacking a six-fold existential puts the whole description under it into normal form, and the description under it reaches the tower; generic in the body nothing unfolds, and the two readings are one line each. This is the same law the previous chapters met on a sentence and on a constructor, met again on a block of binders.

module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where
  Below : Type (ℓ-suc ℓ)
  Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩
        ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
            ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
              × Differs P a₁ e₁ e₂ γ ) ) )

  ≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
  ≺At-in (inl h) =
    ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁
  ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁
  ≺At-in (inr (q , inr (q' , h))) =
    ∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁

  ≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁
  ≺At-out = PT.rec squash₁ outer
    where
    inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
          ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
            × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ )
          → ∥ Below ∥₁
    inner q (inl h) = ∣ inr (q , inl h) ∣₁
    inner q (inr (q' , h)) =
      PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)

    outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩
          ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
            × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂)
                    ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ )
          → ∥ Below ∥₁
    outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁
    outer (inr (q , h)) = PT.rec squash₁ (inner q) h

private
  s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n))))))
  s6a = suc (suc (suc (suc (suc zero))))
  a6a = suc (suc (suc (suc zero)))
  e6a = suc (suc (suc zero))
  s6b = suc (suc zero)
  a6b = suc zero
  e6b = zero

LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n
            → Fin n → Fin n → Fin n → Fin n → Formula S n
LeastNameAt R P B C C₀ s a e d =
  NameAt B C C₀ s a e d
  ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)
                      (suc (suc zero)) (suc zero) zero (sh3 d)
             ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                        (sh3 s) (sh3 a) (sh3 e)) )))


∃₆ : ∀ {n} → Formula S (suc (suc (suc (suc (suc (suc n)))))) → Formula S n
∃₆ φ = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ φ)))))

module _ {n : ℕ} (φ : Formula S (suc (suc (suc (suc (suc (suc n))))))) (γ : S ^ n)
         where
  Six : Type (ℓ-suc ℓ)
  Six = Σ[ s₁ ∈ S ] Σ[ k₁ ∈ S ] Σ[ p₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ k₂ ∈ S ] Σ[ p₂ ∈ S ]
          ⟨ (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) ⊨ φ ⟩

  ∃₆-in : Six → ⟨ γ ⊨ ∃₆ φ ⟩
  ∃₆-in (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , h)))))) =
    ∣ s₁ , ∣ k₁ , ∣ p₁ , ∣ s₂ , ∣ k₂ , ∣ p₂ , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁

  ∃₆-out : ⟨ γ ⊨ ∃₆ φ ⟩ → ∥ Six ∥₁
  ∃₆-out = PT.rec squash₁ at₁
    where
    Body : (s₁ k₁ p₁ s₂ k₂ p₂ : S) → Type (ℓ-suc ℓ)
    Body s₁ k₁ p₁ s₂ k₂ p₂ = ⟨ (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) ⊨ φ ⟩

    at₆ : (s₁ k₁ p₁ s₂ k₂ : S)
        → Σ[ p₂ ∈ S ] Body s₁ k₁ p₁ s₂ k₂ p₂ → ∥ Six ∥₁
    at₆ s₁ k₁ p₁ s₂ k₂ (p₂ , h) = ∣ s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , h))))) ∣₁

    at₅ : (s₁ k₁ p₁ s₂ : S)
        → Σ[ k₂ ∈ S ] ∥ Σ[ p₂ ∈ S ] Body s₁ k₁ p₁ s₂ k₂ p₂ ∥₁ → ∥ Six ∥₁
    at₅ s₁ k₁ p₁ s₂ (k₂ , h) = PT.rec squash₁ (at₆ s₁ k₁ p₁ s₂ k₂) h

    at₄ : (s₁ k₁ p₁ : S)
        → Σ[ s₂ ∈ S ] ∥ Σ[ k₂ ∈ S ]
            ∥ Σ[ p₂ ∈ S ] Body s₁ k₁ p₁ s₂ k₂ p₂ ∥₁ ∥₁ → ∥ Six ∥₁
    at₄ s₁ k₁ p₁ (s₂ , h) = PT.rec squash₁ (at₅ s₁ k₁ p₁ s₂) h

    at₃ : (s₁ k₁ : S)
        → Σ[ p₁ ∈ S ] ∥ Σ[ s₂ ∈ S ] ∥ Σ[ k₂ ∈ S ]
            ∥ Σ[ p₂ ∈ S ] Body s₁ k₁ p₁ s₂ k₂ p₂ ∥₁ ∥₁ ∥₁ → ∥ Six ∥₁
    at₃ s₁ k₁ (p₁ , h) = PT.rec squash₁ (at₄ s₁ k₁ p₁) h

    at₂ : (s₁ : S)
        → Σ[ k₁ ∈ S ] ∥ Σ[ p₁ ∈ S ] ∥ Σ[ s₂ ∈ S ] ∥ Σ[ k₂ ∈ S ]
            ∥ Σ[ p₂ ∈ S ] Body s₁ k₁ p₁ s₂ k₂ p₂ ∥₁ ∥₁ ∥₁ ∥₁ → ∥ Six ∥₁
    at₂ s₁ (k₁ , h) = PT.rec squash₁ (at₃ s₁ k₁) h

    at₁ : Σ[ s₁ ∈ S ] ∥ Σ[ k₁ ∈ S ] ∥ Σ[ p₁ ∈ S ] ∥ Σ[ s₂ ∈ S ] ∥ Σ[ k₂ ∈ S ]
            ∥ Σ[ p₂ ∈ S ] Body s₁ k₁ p₁ s₂ k₂ p₂ ∥₁ ∥₁ ∥₁ ∥₁ ∥₁ → ∥ Six ∥₁
    at₁ (s₁ , h) = PT.rec squash₁ (at₂ s₁) h

StepBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
         → Formula S (suc (suc (suc (suc (suc (suc n))))))
StepBody R P B C C₀ x y =
    LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x)
  ∧̇ ( LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y)
    ∧̇ ≺At (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b )

StepAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
StepAt R P B C C₀ x y = ∃₆ (StepBody R P B C C₀ x y)

module _ {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) where
  StepOf : Type (ℓ-suc ℓ)
  StepOf = Six (StepBody R P B C C₀ x y) γ

  StepAt-in : StepOf → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
  StepAt-in = ∃₆-in (StepBody R P B C C₀ x y) γ

  StepAt-out : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ StepOf ∥₁
  StepAt-out = ∃₆-out (StepBody R P B C C₀ x y) γ