Agreement of environment sets

The satisfaction clauses need, inside L, a single set containing exactly the environments of a given length over a given base set. Earlier chapters supplied two separate pieces: envSetAt, the formula characterizing such a set by its members, and envSet B m, the set constructed in the previous chapter. A set satisfies the description exactly when each of its members is, as a set, the graph of a length-m environment over the base. This chapter proves that the description and the constructed set agree, and the agreement has two readings. A set that a satisfaction judgment has placed at the description's set slot has precisely the members of the constructed set; and the constructed set itself satisfies the description, so a clause that binds its own base and length may fill its slots with the constructed data and quote the description.

Both readings rest on one object, the environment recovered from a member. The four internal clauses, single-valuedness, a numeral domain, values in the base, and pairs made of numerals and base members, say of a set that it is such a graph; from them the previous chapter recovered the assigning function and identified the set with the canonical graph of that function. Here every step reduces to running that recovery in one direction or the other, and to the transport lemma that carries a satisfaction of the environment clause between environments whose named slots agree.

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

The book’s standing options remain in force. This chapter’s only nonconstructive input appears explicitly as the parameter lem below.

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

The basic vocabulary arrives as a whole, as the Prelude arranged. Excluded middle enters as data rather than as an option, and the chapter receives it as a parameter.

module L.Coding.EnvironmentAgreement {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The module parameter is an instance of excluded middle at level ℓ-suc ℓ, the level at which the satisfaction statements of the two structures live. It is forwarded to the chapter whose constructed set this chapter quotes.

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

Two structures interpret the language, and the chapter moves between them. The ambient structure 𝒮ᵥ is the hierarchy itself; the inner structure 𝒮ʟ restricts it to the constructible sets, the class named by isL. The class is transitive, recorded by isL-trans, and the absoluteness machinery is imported to work over exactly this pair.

open import L.Coding.Model {ℓ} using ( envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( envSetAt; extAt-out; extAt-in; extAt-in-both; numL )

Two formulas and their readers do the chapter's work. The environment clause envOverAt says that the candidate graph is single-valued, has exactly the set in the named domain slot as its domain, takes values in the named base set, and contains only pairs drawn from those two sets; the transport lemma moves a satisfaction of this clause between environments whose named slots agree. The extensional description envSetAt says of a set that its members are exactly the environments, in the form of two universally quantified implications, and the three readers unpack those implications in either direction.

open import L.Coding.EnvironmentSet {ℓ} lem
  using ( envSet; envSet-in; envSet-out; envS; envOver; module Recover )

From the previous chapter come the constructed set envSet, its two membership lemmas, the canonical graph element envS, the environment clause envOver satisfied at its own canonical environment, and the recovery module that reads an environment off the four clauses and identifies the set with that environment's graph.

import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_ )

Decoding membership in an environment set into a representing environment returns only a truncated witness, while the target satisfaction and membership statements are propositions. The ambient numerals # m fill the length slots.

open hPropStructure 𝒮ʟ

Opening the inner structure fixes the satisfaction notation used throughout: members of its carrier, its membership, and satisfaction judgments read in L.

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

The absoluteness module is instantiated over the transitive class of constructible sets, and its inner satisfaction relation is renamed to the plain _⊨_, since this chapter reads every formula over L and no other reading competes with it.

From the description to membership

The first module fixes a base set B, an environment γ of some length k, three of its slots, a length m, and two equations saying that the length slot is filled by the numeral of m and the base slot by B. Its hypothesis is that γ satisfies the description with the set slot at Ei. The conclusion is an agreement of members: the set named at Ei and the constructed envSet B m contain exactly the same sets.

Both directions run on the same two ingredients. The recovery module reads an environment off the four clauses and identifies the set it came from with the canonical graph of that environment; the transport lemma carries a satisfaction of the environment clause between environments whose named slots agree, along exactly those naming equations. Neither direction re-proves the description or the construction.

private
  nn : ℕ → S
  nn j = # j , numL j

The length slot is filled by a numeral, and the numeral must itself be an element of L. The helper nn forms it: the ambient von Neumann numeral # j paired with its constructibility proof.

module Ambient (B : S) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (m : ℕ)
  (qd : fst (lookup di γ) ≡ # m) (qb : fst (lookup bi γ) ≡ fst B)
  (hE : ⟨ γ ⊨ envSetAt Ei di bi ⟩) where

The module gathers the data of one instance of the question. B is the base set, γ an environment of length k, and three of its slots are named: Ei holds the candidate set, di holds the numeral of the length, bi holds the base. The equations qd and qb say that these two slots really are filled by the numeral of m and by B, and hE says that γ satisfies the description with the set slot at Ei. Under these data, the set at Ei and envSet B m are shown to have the same members.

  into : (z : S) → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
       → ⟨ fst z ∈ fst (envSet B m) ⟩

The first direction reads the slot set inward: any member of the set named at Ei is a member of the constructed envSet B m.

  into z hz = subst (λ w → ⟨ w ∈ fst (envSet B m) ⟩)
    (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))
    (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))

The proof reuses the recovery of the previous chapter, pointed at the member itself. The hypothesis says that z belongs to the set at Ei, so the description applies at z: the recovery reads off z an environment g whose canonical graph is, as a set, z itself. The constructed set contains the canonical graph of every such environment, and transporting along that identification puts the member z into envSet B m.

    where
    ov : ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
    ov = extAt-out Ei (envOverAt zero (suc di) (suc bi)) γ hE z hz

The recovery needs the four clauses to hold at z, and the description supplies exactly that: applied at the member z, it yields the environment clause over the environment extended by z, with the length and base slots shifted past the new entry.

  outof : (z : S) → ⟨ fst z ∈ fst (envSet B m) ⟩
        → ⟨ fst z ∈ fst (lookup Ei γ) ⟩

The second direction reads outward: any member of the constructed envSet B m is a member of the set named at Ei.

  outof z hz = PT.rec (snd (fst z ∈ fst (lookup Ei γ)))
    (λ { (g , eg) →

Membership in the constructed set hands over a truncated witness: an environment g whose canonical graph is z. The goal, being a membership statement, is a proposition, so the truncation may be consumed, and the membership characterization of the previous chapter is what produces the witness.

      extAt-in Ei (envOverAt zero (suc di) (suc bi)) γ hE z
        (envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)
          (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
          (sym eg) (sym qd) (sym qb)
          (envOver B g)) })

The recovered environment satisfies the environment clause at its own canonical environment, where the three slots hold B, the numeral of m, and its graph. The transport lemma moves that satisfaction to the extended environment (z ∷ γ) along the three equations, reading the canonical graph as z, the numeral as the entry at di, and B as the entry at bi. The description then applies, through its inward implication, to conclude that z belongs to the set at Ei.

    (envSet-out B m z hz)

The environment handed to the transport comes from the membership characterization of the constructed set, applied at the member z with which this direction began.

The constructed set satisfies the description

The second module turns the agreement around and asks the producing question: does the constructed environment set itself satisfy the description? Placed at the set slot, with the numeral of m and the base at the other two slots, it does, and this is what a clause that binds its own base and length needs when it fills those slots with the constructed data. The proof runs the same two moves as before, now in the order the description demands: every member of the constructed set is shown to satisfy the per-member clause, and every set satisfying that clause is shown to be a member.

The module assumes no satisfaction hypothesis. Its three equations say that the set slot holds the constructed set itself, the length slot holds the numeral of m, and the base slot holds B; from these alone the full description at γ is proved.

module AmbientHolds (B : S) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (m : ℕ)
  (qE : fst (lookup Ei γ) ≡ fst (envSet B m))
  (qd : fst (lookup di γ) ≡ # m) (qb : fst (lookup bi γ) ≡ fst B)
  where

The three equations are the whole hypothesis. Naming the set slot with the constructed set, the length slot with the numeral, and the base slot with the base is exactly what a clause does when it fills the three slots with constructed data, so the module proves the description in precisely the form such a clause consumes.

  holds : ⟨ γ ⊨ envSetAt Ei di bi ⟩
  holds = extAt-in-both Ei (envOverAt zero (suc di) (suc bi)) γ fwd bwd

The description is an extensional one: it says that the set at Ei contains exactly the environments, and its two universally quantified implications are proved separately and joined. This is the shape announced at the module head, now filled in.

    where
    fwd : (z : S) → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
        → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩

The forward implication is the producing direction: every member of the constructed set satisfies the per-member clause over the extended environment.

    fwd z hz = PT.rec (snd ((z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi)))
      (λ { (g , eg) → envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)

The membership hz is first re-pointed at the constructed set along the equation qE, and the membership lemma of the previous chapter then hands over a truncated environment. The goal on the other side is a proposition, being one clause of a satisfaction judgment, so the truncated witness can be taken apart.

             (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
             (sym eg) (sym qd) (sym qb) (envOver B g) })

The environment clause of the recovered environment is transported, exactly as in the reading direction, from its canonical environment to the extended environment of the judgment: the graph is read as the member z, the numeral as the entry at di, the base as the entry at bi. What remains is the clause itself, which is what the forward implication owes.

      (envSet-out B m z (subst (λ w → ⟨ fst z ∈ w ⟩) qE hz))

The environment handed to the transport comes from the membership characterization of the constructed set, with qE supplying the first step that reads the member as a member of envSet B m.

    bwd : (z : S) → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
        → ⟨ fst z ∈ fst (lookup Ei γ) ⟩

The backward implication is the reading direction: whatever satisfies the per-member clause over the extended environment belongs to the set at Ei.

    bwd z h = subst (λ w → ⟨ fst z ∈ w ⟩) (sym qE)
      (subst (λ w → ⟨ w ∈ fst (envSet B m) ⟩)
        (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb h))
        (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb h)))

The clause at z is the recovery's input: the recovered environment's canonical graph agrees with z as a set, and the constructed set contains that graph. The first transport reads the recovered graph as z, so the membership lands in envSet B m; the second runs backward along qE and turns membership in envSet B m into membership in the set at Ei.