Constructible codes and subformula trees

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

This chapter proves that term codes, formula codes, and finite environment graphs belong to L, then builds a constructible tree that gathers data over every subformula and characterizes its members.

A code is a hereditarily finite set built by pairing numerals, so it ought to be an element of L, and this chapter says so. The proof is one induction over the formula constructors with nothing in it, but the statement is what lets a later chapter treat a code as an ordinary element of the model rather than as a set of the hierarchy that happens to be lying around.

It matters more than it looks. A recursion internalized in L takes its domain from a small family of elements of L, and the family here is the codes; a graph naming a code as a constant needs that code to be an element of the model, since the object language of the model has no other kind of constant. Both requirements are this one lemma.

This chapter establishes constructibility of individual codes. The set of all codes over a constructible alphabet is constructed later as AllCodes in L.Coding.CodeSet; it supplies the internal syntax domain needed by the definable powerset construction.

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

open import Base.Prelude

module L.Coding.CodeConstructibility {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
open import V.Coding {ℓ} using ( pr; pr-inj; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; IsOrd; Lset )
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; pairʟ-fst; unionʟ; unionʟ-fst )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Axioms.Basic {ℓ} using ( finSet; module FinOf )

open import Cubical.Data.FinData using ( toℕ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_⁆s; ⁅_,_⁆; ⋃_; _∪_; module InfinitySet )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Unit using ( Unit*; tt* )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import V.Model {ℓ} using ( pair-singleton; pair-spec; union-spec )
open InfinitySet using ( #_; sucV )

open hPropStructure 𝒮ʟ using ( S )

Constructible pairs and tags

prL closes constructibility under coded pairing, and tagL specializes it to a numeral tag. These two lemmas cover the outer shape of every syntax constructor.

A numeral is constructible for the same reason, but the result was already used a chapter earlier, so its proof is given there. A pair is constructible because the model has pairing, and the same equation reads it back. A tag is a pair with a numeral on the left, so it is both.

Both are the same two steps: build the thing inside the model, then transport its membership along the equation saying that reading it out gives the thing.

prL : {a b : V ℓ} → ⟨ isL a ⟩ → ⟨ isL b ⟩ → ⟨ isL (pr a b) ⟩
prL {a} {b} pa pb =
  subst (λ w → ⟨ isL w ⟩) (prʟ-fst (a , pa) (b , pb))
    (prʟ (a , pa) (b , pb) .snd)

tagL : (k : ℕ) {x : V ℓ} → ⟨ isL x ⟩ → ⟨ isL (VCode.mkTag k x) ⟩
tagL k px = prL (numL k) px

Induction over term and formula codes

Assuming each constant denotes a constructible set, codeTmL and codeL prove by structural induction that every mapped term and formula code is constructible.

Terms first. A term is a variable or a constant, and the two are the two tags that terms carry: a numeral for the variable's index, and the constant's own set for a constant. So a code is constructible provided the constants it names are, and the induction takes that as its hypothesis rather than assuming there are none.

That generality takes one extra clause and covers the parameters. A formula whose constants are members of a stage codes to a set of L exactly as a parameter-free one does, which is what lets the recursion below range over the formulas the constructible hierarchy is actually built from. The parameter-free case is the instance at the empty type.

Then the formulas: ten clauses with no real content. Each constructor's code is a tag on either a pair of sub-codes, a single sub-code, or a numeral, and the three blocks above cover all three shapes. The induction is over the parameter-free formula rather than its embedding, which requires no extra argument because embedding is a relabelling and commutes with every constructor definitionally.

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

  codeTmL : ∀ {n} (t : Term K n) → ⟨ isL VCode.⌜ mapTm f t ⌝ᵗ ⟩
  codeTmL (con c) = tagL 0 (h c)
  codeTmL (var i) = tagL 1 (numL _)

  codeL : ∀ {n} (φ : Formula K n) → ⟨ isL VCode.⌜ mapFo f φ ⌝ ⟩
  codeL (t ∈̇ u)  = tagL 0  (prL (codeTmL t) (codeTmL u))
  codeL (t ≐ u)  = tagL 1  (prL (codeTmL t) (codeTmL u))
  codeL (φ ∧̇ ψ)  = tagL 2  (prL (codeL φ) (codeL ψ))
  codeL (φ ∨̇ ψ)  = tagL 3  (prL (codeL φ) (codeL ψ))
  codeL (φ ⇒̇ ψ)  = tagL 4  (prL (codeL φ) (codeL ψ))
  codeL ⊥̇        = tagL 5 (numL 0)
  codeL (∃̇ φ)    = tagL 6 (codeL φ)
  codeL (∀̇ φ)    = tagL 7 (codeL φ)
  codeL (∀̇∈ t φ) = tagL 8 (prL (codeTmL t) (codeL φ))
  codeL (∃̇∈ t φ) = tagL 9 (prL (codeTmL t) (codeL φ))

Constructibility of environment graphs

envIsFinSet identifies an environment graph with a finite set of coded pairs, and envL uses a common ordinal stage for those pairs to place the graph in L.

An environment is a finite set: the keys are the numerals below its length and the entries are pairs. It is, in fact, the finite set of the pairs, on the nose, because both are the same image of the same lifted index type. Saying so is one line, and it is the line that lets the finite-family lemma apply to environments without any further argument.

The consequence is that an environment over a stage is an element of L immediately: its entries are pairs of a numeral with a member of the stage, and both are in the stage after one step. No recursion on the length, and no replacement.

envIsFinSet : ∀ {n} (g : Fin n → V ℓ)
            → env g ≡ finSet n (λ i → pr (# (toℕ i)) (g i))
envIsFinSet g = refl

envL : (σ : V ℓ) (oσ : IsOrd σ) {n : ℕ} (g : Fin n → V ℓ)
     → ((i : Fin n) → ⟨ pr (# (toℕ i)) (g i) ∈ Lset σ ⟩)
     → ⟨ isL (env g) ⟩
envL σ oσ {n} g h =
  subst (λ w → ⟨ isL w ⟩) (sym (envIsFinSet g))
    (FinOf.finSetL σ oσ n (λ i → pr (# (toℕ i)) (g i)) h)

Unions and singletons

The singleton and binary-union constructors are implemented both for underlying hierarchy sets and for elements of L, with introduction and elimination lemmas that expose their membership.

Two more shapes, and the model supplies both directly. A singleton is the pair of a thing with itself, and a binary union is the union of the pair, so each is the model's own operation read through the underlying set.

Each shape comes twice over. Once on the underlying set, with the two lemmas that read a member of a singleton or of a binary union back, and once on the model's own sets, where a proof of constructibility accompanies each step and the same lemmas are restated through the equation that reads the underlying set out. The recursion below runs on the second, so a set it builds is an element of L by construction and not by a second induction.

sgl-out : (a x : V ℓ) → ⟨ x ∈ ⁅ a ⁆s ⟩ → x ≡ a
sgl-out a x h = PT.rec (setIsSet x a) (λ { (inl e) → e ; (inr e) → e })
  (subst ⟨_⟩ (pair-spec a a x)
    (subst (λ w → ⟨ x ∈ w ⟩) (sym (pair-singleton a)) h))

sgl-in : (a x : V ℓ) → x ≡ a → ⟨ x ∈ ⁅ a ⁆s ⟩
sgl-in a x e = subst (λ w → ⟨ x ∈ w ⟩) (pair-singleton a)
  (subst ⟨_⟩ (sym (pair-spec a a x)) ∣ inl e ∣₁)

cup-out : (A B x : V ℓ) → ⟨ x ∈ (A ∪ B) ⟩ → ∥ (⟨ x ∈ A ⟩ ⊎ ⟨ x ∈ B ⟩) ∥₁
cup-out A B x h = PT.rec squash₁
  (λ { (v , v∈ , x∈v) → PT.map
         (λ { (inl e) → inl (subst (λ w → ⟨ x ∈ w ⟩) e x∈v)
            ; (inr e) → inr (subst (λ w → ⟨ x ∈ w ⟩) e x∈v) })
         (subst ⟨_⟩ (pair-spec A B v) v∈) })
  (subst ⟨_⟩ (union-spec ⁅ A , B ⁆ x) h)

cup-inl : (A B x : V ℓ) → ⟨ x ∈ A ⟩ → ⟨ x ∈ (A ∪ B) ⟩
cup-inl A B x h = subst ⟨_⟩ (sym (union-spec ⁅ A , B ⁆ x))
  ∣ A , subst ⟨_⟩ (sym (pair-spec A B A)) ∣ inl refl ∣₁ , h ∣₁

cup-inr : (A B x : V ℓ) → ⟨ x ∈ B ⟩ → ⟨ x ∈ (A ∪ B) ⟩
cup-inr A B x h = subst ⟨_⟩ (sym (union-spec ⁅ A , B ⁆ x))
  ∣ B , subst ⟨_⟩ (sym (pair-spec A B B)) ∣ inr refl ∣₁ , h ∣₁

sglʟ : S → S
sglʟ a = pairʟ a a

sglʟ-fst : (a : S) → fst (sglʟ a) ≡ ⁅ fst a ⁆s
sglʟ-fst a = pairʟ-fst a a ∙ pair-singleton (fst a)

cupʟ : S → S → S
cupʟ a b = unionʟ (pairʟ a b)

cupʟ-fst : (a b : S) → fst (cupʟ a b) ≡ (fst a ∪ fst b)
cupʟ-fst a b = unionʟ-fst (pairʟ a b) ∙ cong (⋃_) (pairʟ-fst a b)

sglʟ-in : (a : S) (x : V ℓ) → x ≡ fst a → ⟨ x ∈ fst (sglʟ a) ⟩
sglʟ-in a x e = subst (λ w → ⟨ x ∈ w ⟩) (sym (sglʟ-fst a)) (sgl-in (fst a) x e)

sglʟ-out : (a : S) (x : V ℓ) → ⟨ x ∈ fst (sglʟ a) ⟩ → x ≡ fst a
sglʟ-out a x h = sgl-out (fst a) x (subst (λ w → ⟨ x ∈ w ⟩) (sglʟ-fst a) h)

cupʟ-inl : (a b : S) (x : V ℓ) → ⟨ x ∈ fst a ⟩ → ⟨ x ∈ fst (cupʟ a b) ⟩
cupʟ-inl a b x h = subst (λ w → ⟨ x ∈ w ⟩) (sym (cupʟ-fst a b))
  (cup-inl (fst a) (fst b) x h)

cupʟ-inr : (a b : S) (x : V ℓ) → ⟨ x ∈ fst b ⟩ → ⟨ x ∈ fst (cupʟ a b) ⟩
cupʟ-inr a b x h = subst (λ w → ⟨ x ∈ w ⟩) (sym (cupʟ-fst a b))
  (cup-inr (fst a) (fst b) x h)

cupʟ-out : (a b : S) (x : V ℓ) → ⟨ x ∈ fst (cupʟ a b) ⟩
         → ∥ (⟨ x ∈ fst a ⟩ ⊎ ⟨ x ∈ fst b ⟩) ∥₁
cupʟ-out a b x h = cup-out (fst a) (fst b) x
  (subst (λ w → ⟨ x ∈ w ⟩) (cupʟ-fst a b) h)

The subformula recursion

tree f φ unions the value f χ over every subformula χ of φ; tree-inv describes any member by the subformula that contributed it, while Parts records the forward inclusions.

One recursion over the ten constructors, with what it collects left as its parameter. It gathers one thing per subformula: give it the key and it gives the subformula closure of the next section, give it an entry and it gives the satisfaction table of a later chapter. Both want the same inversion, so the inversion is proved here once and instantiated twice.

Of says what a member of such a set is: one of the things gathered, gathered at some subformula whose own set sits inside the one it came from. tree-inv proves it, and Parts carries the memberships the other direction needs, one for each shape a clause of the recursion produces.

module _ {ℓ' : Level} {K : Type ℓ'} where

  tree : (∀ {m} → Formula K m → S) → ∀ {n} → Formula K n → S
  tree f φ@(t ∈̇ u)  = sglʟ (f φ)
  tree f φ@(t ≐ u)  = sglʟ (f φ)
  tree f φ@⊥̇        = sglʟ (f φ)
  tree f φ@(a ∧̇ b)  = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
  tree f φ@(a ∨̇ b)  = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
  tree f φ@(a ⇒̇ b)  = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
  tree f φ@(∃̇ a)    = cupʟ (sglʟ (f φ)) (tree f a)
  tree f φ@(∀̇ a)    = cupʟ (sglʟ (f φ)) (tree f a)
  tree f φ@(∀̇∈ t a) = cupʟ (sglʟ (f φ)) (tree f a)
  tree f φ@(∃̇∈ t a) = cupʟ (sglʟ (f φ)) (tree f a)

  Of : (f g : ∀ {m} → Formula K m → S) {n : ℕ} → Formula K n → V ℓ
     → Type (ℓ-max (ℓ-suc ℓ) ℓ')
  Of f g φ x = ∥ (Σ[ m ∈ ℕ ] Σ[ χ ∈ Formula K m ]
                   ((x ≡ fst (f χ))
                    × ((z : V ℓ) → ⟨ z ∈ fst (tree g χ) ⟩
                       → ⟨ z ∈ fst (tree g φ) ⟩))) ∥₁

  private
    module _ (f g : ∀ {m} → Formula K m → S) where
      one : ∀ {n} (φ : Formula K n) (x : V ℓ)
          → ⟨ x ∈ fst (sglʟ (f φ)) ⟩ → Of f g φ x
      one {n} φ x h = ∣ n , φ , sglʟ-out (f φ) x h , (λ _ hz → hz) ∣₁

      wider : ∀ {n m} (φ : Formula K n) (χ : Formula K m) {x : V ℓ}
            → ((z : V ℓ) → ⟨ z ∈ fst (tree g χ) ⟩ → ⟨ z ∈ fst (tree g φ) ⟩)
            → Of f g χ x → Of f g φ x
      wider _ _ s = PT.map
        (λ { (m , ψ , e , t) → m , ψ , e , (λ z hz → s z (t z hz)) })

      un : ∀ {n m} (φ : Formula K n) (a : Formula K m)
         → ((z : V ℓ) → ⟨ z ∈ fst (cupʟ (sglʟ (g φ)) (tree g a)) ⟩
            → ⟨ z ∈ fst (tree g φ) ⟩)
         → ((x : V ℓ) → ⟨ x ∈ fst (tree f a) ⟩ → Of f g a x)
         → (x : V ℓ) → ⟨ x ∈ fst (cupʟ (sglʟ (f φ)) (tree f a)) ⟩ → Of f g φ x
      un φ a into ra x h = PT.rec squash₁
        (λ { (inl e) → one φ x e
           ; (inr e) → wider φ a
               (λ z hz → into z (cupʟ-inr (sglʟ (g φ)) (tree g a) z hz))
               (ra x e) })
        (cupʟ-out (sglʟ (f φ)) (tree f a) x h)

      bin : ∀ {n m} (φ : Formula K n) (a b : Formula K m)
          → ((z : V ℓ)
             → ⟨ z ∈ fst (cupʟ (sglʟ (g φ)) (cupʟ (tree g a) (tree g b))) ⟩
             → ⟨ z ∈ fst (tree g φ) ⟩)
          → ((x : V ℓ) → ⟨ x ∈ fst (tree f a) ⟩ → Of f g a x)
          → ((x : V ℓ) → ⟨ x ∈ fst (tree f b) ⟩ → Of f g b x)
          → (x : V ℓ)
          → ⟨ x ∈ fst (cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))) ⟩
          → Of f g φ x
      bin φ a b into ra rb x h = PT.rec squash₁
        (λ { (inl e) → one φ x e
           ; (inr e) → PT.rec squash₁
               (λ { (inl ea) → wider φ a (λ z hz → into z
                      (cupʟ-inr (sglʟ (g φ)) (cupʟ (tree g a) (tree g b)) z
                        (cupʟ-inl (tree g a) (tree g b) z hz)))
                      (ra x ea)
                  ; (inr eb) → wider φ b (λ z hz → into z
                      (cupʟ-inr (sglʟ (g φ)) (cupʟ (tree g a) (tree g b)) z
                        (cupʟ-inr (tree g a) (tree g b) z hz)))
                      (rb x eb) })
               (cupʟ-out (tree f a) (tree f b) x e) })
        (cupʟ-out (sglʟ (f φ)) (cupʟ (tree f a) (tree f b)) x h)

  module Parts (f : ∀ {m} → Formula K m → S) where
    self : ∀ {n} (φ : Formula K n) → ⟨ fst (f φ) ∈ fst (tree f φ) ⟩
    self φ@(t ∈̇ u)  = sglʟ-in (f φ) _ refl
    self φ@(t ≐ u)  = sglʟ-in (f φ) _ refl
    self φ@⊥̇        = sglʟ-in (f φ) _ refl
    self φ@(a ∧̇ b)  = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(a ∨̇ b)  = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(a ⇒̇ b)  = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∃̇ a)    = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∀̇ a)    = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∀̇∈ t a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∃̇∈ t a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)

    left : ∀ {n m} (χ : Formula K n) (a b : Formula K m) (z : V ℓ)
         → ⟨ z ∈ fst (tree f a) ⟩
         → ⟨ z ∈ fst (cupʟ (sglʟ (f χ)) (cupʟ (tree f a) (tree f b))) ⟩
    left χ a b z h = cupʟ-inr (sglʟ (f χ)) (cupʟ (tree f a) (tree f b)) z
                       (cupʟ-inl (tree f a) (tree f b) z h)

    right : ∀ {n m} (χ : Formula K n) (a b : Formula K m) (z : V ℓ)
          → ⟨ z ∈ fst (tree f b) ⟩
          → ⟨ z ∈ fst (cupʟ (sglʟ (f χ)) (cupʟ (tree f a) (tree f b))) ⟩
    right χ a b z h = cupʟ-inr (sglʟ (f χ)) (cupʟ (tree f a) (tree f b)) z
                        (cupʟ-inr (tree f a) (tree f b) z h)

    only : ∀ {n m} (χ : Formula K n) (a : Formula K m) (z : V ℓ)
         → ⟨ z ∈ fst (tree f a) ⟩
         → ⟨ z ∈ fst (cupʟ (sglʟ (f χ)) (tree f a)) ⟩
    only χ a z h = cupʟ-inr (sglʟ (f χ)) (tree f a) z h

  tree-inv : (f g : ∀ {m} → Formula K m → S)
           → ∀ {n} (φ : Formula K n) (x : V ℓ)
           → ⟨ x ∈ fst (tree f φ) ⟩ → Of f g φ x
  tree-inv f g φ@(t ∈̇ u) = one f g φ
  tree-inv f g φ@(t ≐ u) = one f g φ
  tree-inv f g φ@⊥̇       = one f g φ
  tree-inv f g φ@(a ∧̇ b) = bin f g φ a b (λ _ hz → hz)
                             (tree-inv f g a) (tree-inv f g b)
  tree-inv f g φ@(a ∨̇ b) = bin f g φ a b (λ _ hz → hz)
                             (tree-inv f g a) (tree-inv f g b)
  tree-inv f g φ@(a ⇒̇ b) = bin f g φ a b (λ _ hz → hz)
                             (tree-inv f g a) (tree-inv f g b)
  tree-inv f g φ@(∃̇ a)    = un f g φ a (λ _ hz → hz) (tree-inv f g a)
  tree-inv f g φ@(∀̇ a)    = un f g φ a (λ _ hz → hz) (tree-inv f g a)
  tree-inv f g φ@(∀̇∈ t a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)
  tree-inv f g φ@(∃̇∈ t a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)

The subformula closure

Specializing the generic tree to formula keys produces closure φ, a constructible set containing the key of φ and the keys of all its subformulas, together with explicit membership maps for each constructor.

A recursion on codes is stated against a slot: a set of codes closed under immediate subcodes, holding the one the recursion is asked about. The smallest such slot is the set of codes of a formula's own subformulas, and it is the recursion above taken at the key.

Each entry carries its arity, because the recursion's own key does; a binder's subformula therefore enters at the successor. This is the only place where a change of arity appears explicitly, and it appears there because the arity is exactly what the frames bind.

Constructibility is not a second proof. The recursion above runs on the model's own sets, so the certificate comes out of it together with the set.

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

  key : ∀ {n} → Formula K n → V ℓ
  key {n} φ = pr (# n) VCode.⌜ mapFo f φ ⌝

  keyL : ∀ {n} (φ : Formula K n) → ⟨ isL (key φ) ⟩
  keyL φ = prL (numL _) (codeL f h φ)

  private
    keyS : ∀ {m} → Formula K m → S
    keyS φ = key φ , keyL φ

  closure : ∀ {n} → Formula K n → V ℓ
  closure φ = fst (tree keyS φ)

  closureL : ∀ {n} (φ : Formula K n) → ⟨ isL (closure φ) ⟩
  closureL φ = snd (tree keyS φ)

Recap

The results place syntax codes, environments, and subformula-indexed collections inside L; the remaining lemmas turn closure membership back into a concrete subformula key for later bounded recursion.

codeL says every code is an element of L, and numL, prL and tagL are the three shapes it is built from. With it a code may be named as a constant of the model's object language, and a family of codes may be the domain of an internalized recursion.

envL then puts an environment in L with no recursion on its length and no use of replacement, because an environment is on the nose the finite set of its entries. closure is the smallest slot a recursion on a code can be stated against, and closureL reads its certificate off the recursion that built it rather than proving it a second time.

The set of all codes is still not an element of L, and is still not needed.

Reading a closure back

closure-inv applies the generic tree inversion to show that every member of closure φ is the key of some subformula whose closure embeds into that of φ.

A recursion over codes has to know what the elements of its domain are, and "whatever the union of these singletons happens to contain" is not an answer. The lemma below is the answer: every element of a closure is the key of a formula, and that formula's own closure sits inside the one it came from. The second half is what an induction consumes, since it is how the induction knows its hypothesis is available where it wants to apply it.

It and the membership of a key in its own closure are the recursion above read at the key, so neither is an induction here.

  Inv : ∀ {n} → Formula K n → V ℓ → Type (ℓ-suc ℓ)
  Inv φ x = Of keyS keyS φ x

  closure-inv : ∀ {n} (φ : Formula K n) (x : V ℓ)
              → ⟨ x ∈ closure φ ⟩ → Inv φ x
  closure-inv φ x hx = tree-inv keyS keyS φ x hx

  key∈closure : ∀ {n} (φ : Formula K n) → ⟨ key φ ∈ closure φ ⟩
  key∈closure φ = Parts.self keyS φ

Recovering a formula from its key

When a set is known to equal the key of a formula, the final lemma transports that witness into an explicit formula and retains the inclusion of its closure into the original closure.

The demand a closedness predicate makes is indexed by a constructor tag, and the formula it is made of is indexed by a constructor. Matching the two is the only real work in the first instance, and doing it clause by clause would be ten formulas times seven demands. It is not, because the demand can be computed from the tag: one type family over the tag, one function over the formula, and the equation between tags that the key's injectivity yields carries the second to the first.

Below the tag, a key is an arity paired with a code, and both layers are pinned by pairing's injectivity. What comes out is that an arity-preserving constructor demands its components at the arity read, an arity-raising one demands them at the successor, and a constructor with no subformula demands nothing.

  module _ (C : V ℓ) where
    BothSame : V ℓ → V ℓ → Type (ℓ-suc ℓ)
    BothSame ar p = (u v : V ℓ) → p ≡ pr u v
                  → ⟨ pr ar u ∈ C ⟩ × ⟨ pr ar v ∈ C ⟩

    SecondSucc : V ℓ → V ℓ → Type (ℓ-suc ℓ)
    SecondSucc ar p = (u v : V ℓ) → p ≡ pr u v → ⟨ pr (sucV ar) v ∈ C ⟩

    Concl : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
    Concl 2  ar p = BothSame ar p
    Concl 3  ar p = BothSame ar p
    Concl 4  ar p = BothSame ar p
    Concl 6 ar p = ⟨ pr (sucV ar) p ∈ C ⟩
    Concl 7 ar p = ⟨ pr (sucV ar) p ∈ C ⟩
    Concl 8 ar p = SecondSucc ar p
    Concl 9 ar p = SecondSucc ar p
    Concl _  _  _ = Unit*

    private
      Below : ∀ {n} → Formula K n → Type (ℓ-suc ℓ)
      Below φ = (z : V ℓ) → ⟨ z ∈ closure φ ⟩ → ⟨ z ∈ C ⟩

      inC : ∀ {n m} (φ : Formula K n) (a : Formula K m)
          → Below φ → ⟨ key a ∈ closure φ ⟩ → {w : V ℓ} → key a ≡ w → ⟨ w ∈ C ⟩
      inC φ a below mem q = subst (λ w → ⟨ w ∈ C ⟩) q (below (key a) mem)

      atTag : ∀ {m k : ℕ} {ar p : V ℓ} (j : ℕ) (q : V ℓ)
            → pr (# m) (VCode.mkTag j q) ≡ pr ar (pr (# k) p)
            → (j ≡ k) × ((# m ≡ ar) × (q ≡ p))
      atTag j q e = VCode.mkTag-inj (pr-inj e .snd) .fst
                  , (pr-inj e .fst , VCode.mkTag-inj (pr-inj e .snd) .snd)

      bothOf : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
             → Below φ' → ⟨ key a ∈ closure φ' ⟩ → ⟨ key b ∈ closure φ' ⟩
             → (ar p : V ℓ) → # m' ≡ ar
             → pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝ ≡ p
             → BothSame ar p
      bothOf φ' a b below ma mb ar p qa qp u v qu =
          inC φ' a below ma (cong₂ pr qa (pr-inj (qp ∙ qu) .fst))
        , inC φ' b below mb (cong₂ pr qa (pr-inj (qp ∙ qu) .snd))

      oneOf : ∀ {n m'} (φ' : Formula K n) (a : Formula K m')
            → Below φ' → ⟨ key a ∈ closure φ' ⟩
            → (ar p : V ℓ) → # m' ≡ ar → VCode.⌜ mapFo f a ⌝ ≡ p
            → ⟨ pr ar p ∈ C ⟩
      oneOf φ' a below ma ar p qa qp = inC φ' a below ma (cong₂ pr qa qp)

      upOf : ∀ {n m'} (φ' : Formula K n) (a : Formula K (suc m'))
           → Below φ' → ⟨ key a ∈ closure φ' ⟩
           → (ar p : V ℓ) → # m' ≡ ar → VCode.⌜ mapFo f a ⌝ ≡ p
           → ⟨ pr (sucV ar) p ∈ C ⟩
      upOf φ' a below ma ar p qa qp =
        inC φ' a below ma (cong₂ pr (cong sucV qa) qp)

      sndUpOf : ∀ {n m'} (φ' : Formula K n) (t : Term K m')
                (a : Formula K (suc m'))
              → Below φ' → ⟨ key a ∈ closure φ' ⟩
              → (ar p : V ℓ) → # m' ≡ ar
              → pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝ ≡ p
              → SecondSucc ar p
      sndUpOf φ' t a below ma ar p qa qp u v qu =
        inC φ' a below ma (cong₂ pr (cong sucV qa) (pr-inj (qp ∙ qu) .snd))

      left : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
           → ⟨ key a ∈ fst (cupʟ (sglʟ (keyS φ'))
                              (cupʟ (tree keyS a) (tree keyS b))) ⟩
      left φ' a b = Parts.left keyS φ' a b (key a) (key∈closure a)

      right : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
            → ⟨ key b ∈ fst (cupʟ (sglʟ (keyS φ'))
                               (cupʟ (tree keyS a) (tree keyS b))) ⟩
      right φ' a b = Parts.right keyS φ' a b (key b) (key∈closure b)

      only : ∀ {n m'} (φ' : Formula K n) (a : Formula K m')
           → ⟨ key a ∈ fst (cupʟ (sglʟ (keyS φ')) (tree keyS a)) ⟩
      only φ' a = Parts.only keyS φ' a (key a) (key∈closure a)

    byTag : ∀ {m} (φ : Formula K m) (k : ℕ) (ar p : V ℓ)
          → Below φ → key φ ≡ pr ar (pr (# k) p) → Concl k ar p
    byTag (t ∈̇ u) k ar p below eq = subst (λ j → Concl j ar p)
      (atTag 0 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ) eq .fst) tt*
    byTag (t ≐ u) k ar p below eq = subst (λ j → Concl j ar p)
      (atTag 1 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ) eq .fst) tt*
    byTag ⊥̇ k ar p below eq = subst (λ j → Concl j ar p)
      (atTag 5 (# 0) eq .fst) tt*
    byTag φ@(a ∧̇ b) k ar p below eq =
      let r = atTag 2 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (bothOf φ a b below (left φ a b) (right φ a b) ar p
          (r .snd .fst) (r .snd .snd))
    byTag φ@(a ∨̇ b) k ar p below eq =
      let r = atTag 3 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (bothOf φ a b below (left φ a b) (right φ a b) ar p
          (r .snd .fst) (r .snd .snd))
    byTag φ@(a ⇒̇ b) k ar p below eq =
      let r = atTag 4 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (bothOf φ a b below (left φ a b) (right φ a b) ar p
          (r .snd .fst) (r .snd .snd))
    byTag φ@(∃̇ a) k ar p below eq =
      let r = atTag 6 VCode.⌜ mapFo f a ⌝ eq in
      subst (λ j → Concl j ar p) (r .fst)
        (upOf φ a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
    byTag φ@(∀̇ a) k ar p below eq =
      let r = atTag 7 VCode.⌜ mapFo f a ⌝ eq in
      subst (λ j → Concl j ar p) (r .fst)
        (upOf φ a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
    byTag φ@(∀̇∈ t a) k ar p below eq =
      let r = atTag 8 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (sndUpOf φ t a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
    byTag φ@(∃̇∈ t a) k ar p below eq =
      let r = atTag 9 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (sndUpOf φ t a below (only φ a) ar p (r .snd .fst) (r .snd .snd))