---
title: "Agreement of environment sets"
module: L.Coding.EnvironmentAgreement
lang: en
site: "Bedrock"
description: "Agreement of environment sets"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 52
canonical: https://bedrock.institute/en/L.Coding.EnvironmentAgreement.html
html: L.Coding.EnvironmentAgreement.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/EnvironmentAgreement.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Absoluteness, V.Hierarchy, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Coding.EnvironmentSet]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.EnvironmentAgreement.md, https://bedrock.institute/ja/L.Coding.EnvironmentAgreement.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
open hPropStructure 𝒮ʟ
```

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

```agda
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.

```agda
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.

```agda
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.

```agda
  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`.

```agda
  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`.

```agda
    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.

```agda
  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`.

```agda
  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.

```agda
      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`.

```agda
    (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.

```agda
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.

```agda
  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.

```agda
    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.

```agda
    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.

```agda
             (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.

```agda
      (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`.

```agda
    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`.

```agda
    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`.