---
title: "Coding formulas over the constructible model"
module: L.Coding.Model
lang: en
site: "Bedrock"
description: "Coding formulas over the constructible model"
stage: "Internal coding: expressions and domains"
reading_order: 42
canonical: https://bedrock.institute/en/L.Coding.Model.html
html: L.Coding.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Model.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, FOL.Coding, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Absoluteness, L.Coding.PairFormulas, L.Axioms.Numerals]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.Model.md, https://bedrock.institute/ja/L.Coding.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Coding formulas over the constructible model

An element of the constructible model `L` is not a bare set: it is an ambient set of the hierarchy `V ℓ` together with a proof that the set is constructible. So when a first-order formula is evaluated in `L`, its quantifiers range over such pairs, while the set-coded facts one actually wants, membership of a Kuratowski pair in a graph, say, are facts about the underlying sets. This chapter builds the bridge between the two readings.

The bridge has two directions. Projecting an entry outward directly discards its constructibility certificate, while transferring a bounded reader uses the absoluteness guaranteed by transitivity of `L`. Reading inward requires a witness inside the model: from a proof that a pair belongs to a constructible graph, transitivity supplies the constructibility certificate that makes the pair an element of `L`.

On top of the pair reader the chapter assembles the vocabulary of functions-as-graphs, and it is worth seeing that the clauses are logically independent. Graph application only asserts that a given ordered pair belongs to a graph. Single-valuedness says that an argument determines at most one value; it says nothing about which arguments have values. The exact-domain clause and the range restriction each constrain one further aspect. And none of these forbids a candidate graph from carrying extra elements that are not pairs at all, since these three conditions speak only about pair-shaped members; a fourth clause, that every member is a pair of an index and a value, excludes that junk. Together they form `envOverAt`, a predicate on one candidate graph relative to a domain `d` and a range `B`; it says when a given set is an environment over `d` into `B`, and does not construct the set of all environments.

The second half turns to coding. Ordered pairs and numerals can be built inside `L`, and each projects to its ambient counterpart. Since every code is a tag paired with a payload, each internal code projects to the ambient code of the formula whose constants have been projected; this compatibility is what lets the ambient readers of the earlier sections analyze codes built inside the model. A closing observation is that the whole environment description depends on its assignment only through three projected sets, so it transfers unchanged to any other assignment presenting the same graph, domain, and range; and when a code is known to be a pair, transitivity of `L` packages its two components into one constructible set.

The two worlds sit at one universe level `ℓ`. An assignment for the inner language is a vector of elements of the carrier `S`, each an ambient set with its constructibility certificate; an ambient fact, by contrast, is stated about the underlying sets obtained by projecting every entry with `fst`. Every adequacy statement of this chapter takes the form of an identification between a satisfaction judgment at such a paired assignment and a fact about the projected one, and the projections must be handled once, correctly, before any set theory can happen.

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

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )
```

Adequacy statements compare truth values, so the ambient facts are packaged as propositions. In particular, equality of two sets in the hierarchy is a proposition because the hierarchy is an h-set. Paths and congruence then align these packaged equalities with the projected lookups, while the substantive set-theoretic inputs, absoluteness, pairing, and numeral facts, enter in their own lemmas.

```agda
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∀̇_; ∀̇∈; ∃̇_; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
import FOL.Absoluteness
```

Transitivity of `L` enters in two related ways. It underlies the Δ₀ absoluteness used to transfer bounded readers, and it constructs model witnesses from members of constructible sets. A direct projection needs no new witness, but the formula transfer that justifies the outward reading still rests on this transitivity theorem.

```agda
import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import V.Model {ℓ} using ( pair-singleton )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
```

The outward direction for bounded formulas is supplied by absoluteness: a Δ₀ formula about the hierarchy, whose constants name constructible sets, has the same meaning when read in `L`, and the two readings agree by a path. The pair reader is of exactly this kind, so its satisfaction in the model is identified with an equation between projected sets. The inward direction has no general shortcut; it is supplied per entry by an explicit construction of a witness, and the pair case is the one this chapter needs.

```agda
open import L.Absoluteness {ℓ} using ( liftFo; transferFo )
open import L.Coding.PairFormulas {ℓ}
  using ( prAt; Δ₀-prAt; prAt-adequate; ∈pair-introL; ∈pair-introR )
open import L.Axioms.Numerals {ℓ}
  using ( numeralL; numeralL-fst; pairʟ; pairʟ-fst )
```

Some existence statements in the chapter are deliberately weak. When a graph member is said to exist, the claim is merely that some entry exists, not a chosen one: such statements live in propositional truncation and can be eliminated only into proposition-valued targets. Keeping truncated existence distinct from an explicit witness matters in both directions of every adequacy proof, since satisfaction of an existential formula always has the truncated shape.

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( map )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
import Cubical.HITs.PropositionalTruncation as PT
```

Truth values are propositions at level `ℓ-suc ℓ`: a formula does not evaluate to a boolean but to an `hProp`, packaging an underlying type with the proof that it is a proposition. The carrier `S` of the inner structure is thereby fixed as well: its elements are exactly the pairs of an ambient set and a constructibility certificate. Throughout what follows, `γ ⊨ φ` means satisfaction in the constructible model, and `⟦ t ⟧ γ` is an element of `S`, a set with its certificate.

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆ )

open hPropStructure 𝒮ʟ using ( S )
```

One more structural fact shapes the statements: every reader of this chapter is stated through `fst` of a lookup and nothing else. That is, satisfaction in the model is always compared with facts about underlying sets, never with anything internal to the certificates. The same principle makes the final transport lemma possible: if two assignments present the same three underlying sets where a description looks, the description cannot tell the assignments apart.

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

## Looking up in a projected environment

Every adequacy statement of this chapter compares a satisfaction judgment at an assignment of model elements with an ambient fact about the *projected* assignment, in which each entry has been stripped of its constructibility certificate by `fst`. The two assignments are not the same object, so before any comparison can be made one must know that looking up a variable in the projected assignment gives the projection of looking it up in the original. That is the whole content of the lemma below, and it enters every adequacy proof that follows, wherever an ambient equation has to be rephrased in terms of the entries of `γ` themselves.

The proof is a recursion on the position `i`. At position `zero`, both sides reduce to the head of the list: `lookup zero (x ∷ γ)` is `x`, `map fst` of the cons is the cons of the projections, and the two first projections of `x` agree definitionally, hence `refl`. At a successor position, both lookups advance one entry and the recursive call finishes the argument. Nothing here uses constructibility; the lemma holds for any environment of pairs.

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

## The ordered pair

The bridge this chapter builds runs in two directions. Forward, a satisfaction judgment in the model, evaluated at an assignment whose entries are elements of the model, must be converted into a fact about sets of the hierarchy; the entries are first projected by `fst`, so the ambient statement is always about projected values. The first entry of the dictionary is the recognition of ordered pairs: the ambient reader `prAt q u v` says that the value at position `q` is the Kuratowski pair of the values at `u` and `v`. Because this reader is bounded (Δ₀), its meaning is absolute, so reading it in the language of `L` costs nothing; and since it names no constants, the lift imposes no conditions on them. The theorem states the outcome exactly: satisfaction of the lifted reader in the model is a path to the equality of the projected value at `q` with `pr` of the projected values at `u` and `v`. The reverse direction, where a bare ambient membership must be converted back into a witness living inside the model, first appears in the next section, and there transitivity of `L` does the work.

The statement compares truth values, so its right-hand side must be a truth value too. Equality of two sets of the hierarchy is a proposition because the hierarchy is an h-set, and `PairIs` packages such a path type with exactly that propositionhood proof. The lifted reader `prAtL q u v` is `prAt q u v` itself with each constant relabelled into the carrier `S`; here there are no constants to relabel, but the boundedness certificate `Δ₀-prAt` still travels with the formula, since the transfer lemma demands one.

```agda
private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

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

The adequacy statement equates, by a single path, satisfaction of the reader in the model with the packaged equality on the right. Note where the projections stand: the assignment `γ` consists of elements of `S`, and the equation is stated about `fst` of the looked-up entries. That is the shape every entry of this dictionary takes, because the concrete membership facts live in the hierarchy, not inside the model's carrier.

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

The proof composes three paths and introduces nothing new. The transfer lemma first equates satisfaction in `L` with ambient satisfaction of `prAt q u v` at the projected assignment, using the boundedness certificate. The reader's own adequacy theorem then rewrites that ambient satisfaction as the equality of the interpreted values. Finally the two lookups of the projected assignment are moved to projections of the lookups in `γ`, and the equation is reassembled under `PairIs` by congruence. The result is exactly the promised identification.

```agda
  ∙ prAt-adequate q u v (map fst γ)
  ∙ cong₂ PairIs (lookup-fst q γ)
      (cong₂ pr (lookup-fst u γ) (lookup-fst v γ))
```

## Application

A graph in the object language is a set of ordered pairs, and the question every later use asks of one is whether a given pair belongs to it. The reader below expresses exactly that as a bounded existential, over the members of whatever set a term denotes, with the pair reader as its body. Its meaning is the ambient membership of the Kuratowski pair in the graph's underlying set.

The forward direction converts satisfaction into membership. The backward direction is where the model does real work: to satisfy the existential one must produce an *element of the model* whose underlying set is the pair, while the hypothesis supplies only a set. The pair is constructible because it belongs to a constructible set and the constructible class is transitive. This one step is the whole argument, and it recurs wherever a witness must be produced inside the model rather than merely in the hierarchy.

The definition reads: there merely exists a member of the graph, bounded by the value of the term `F`, satisfying the pair reader. The bound entry of the existential extends the environment, and the three positions of the pair reader name that entry together with the shifted references to the two arguments, while the bound `F` denotes the graph over which the fresh entry ranges.

```agda
private
  appTerm : ∀ {n} → Term S n → Fin n → Fin n → Formula S n
  appTerm F x y = ∃̇∈ F (prAtL zero (suc x) (suc y))

  appTerm-adequate : ∀ {n} (F : Term S n) (x y : Fin n) (γ : S ^ n)
    → (γ ⊨ appTerm F x y)
```

The adequacy statement names the ingredients. Here `a` and `b` are the projected values of the two argument slots, and `G` is the interpretation of the term: an element of `S`, hence a set carrying its constructibility certificate, whose underlying set is the graph. The claim is a path of truth values between satisfaction and an ambient membership: the pair `pr a b` belongs to the underlying set of the graph.

```agda
    ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (⟦ F ⟧ γ))
  appTerm-adequate F x y γ = ⇔toPath fwd bwd
    where
    a = fst (lookup x γ)
    b = fst (lookup y γ)
```

The auxiliary `read` unpacks one existential fiber. Given an element `z` of the model and a proof that the extended assignment satisfies the pair reader, the adequacy theorem already proved for the pair reader transports that proof to the proposition that the underlying set of `z` equals `pr a b`. The forward direction receives, after unfolding the bounded existential's satisfaction, a truncated pair of a membership `z∈G` and such a reader proof; eliminating the truncation is legitimate because the target membership is a proposition, and inside the branch the membership is transported along the path that `read` supplies.

```agda
    G = ⟦ F ⟧ γ

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

    fwd : ⟨ γ ⊨ appTerm F x y ⟩ → ⟨ pr a b ∈ fst G ⟩
    fwd = PT.rec (snd (pr a b ∈ fst G))
```

The backward direction is where the constructible model enters. From a bare membership proof `⟨ pr a b ∈ fst G ⟩` one must produce a proof of the truncated existential, and its first component cannot be the set `pr a b` itself, which is a set of the hierarchy and not an element of `S`. The witness is built in the next lines; the displayed branch packages the membership with a reader proof obtained by transporting `refl` backwards through the adequacy path, which is legitimate because the underlying set of the witness is definitionally `pr a b`.

```agda
      (λ { (z , (z∈G , h)) → subst (λ w → ⟨ w ∈ fst G ⟩) (read z h) z∈G })

    bwd : ⟨ pr a b ∈ fst G ⟩ → ⟨ γ ⊨ appTerm F x y ⟩
    bwd h = ∣ zS , (h , subst ⟨_⟩
        (sym (prAtL-adequate zero (suc x) (suc y) (zS ∷ γ))) refl) ∣₁
      where
```

The witness is the one genuinely model-specific construction of this section. To present `pr a b` as an element of `S`, one needs a constructibility certificate for it. The hypothesis says the pair belongs to the underlying set of `G`, and `G` carries its own certificate; transitivity of the constructible class turns these two facts into `isL (pr a b)`. A member of a constructible set is constructible. With the witness in place, the public form `appAt` fixes the graph to sit in a variable slot, reading the term `var f`, and its adequacy is just the general theorem at that particular term: membership of the projected pair in the underlying set of the value at slot `f`.

```agda
      zS : S
      zS = pr a b , isL-trans {x = fst G} {y = pr a b} h (G .snd)

appAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
appAt f = appTerm (var f)

appAt-adequate : ∀ {n} (f x y : Fin n) (γ : S ^ n)
```

This specialization matters because the remaining graph predicates refer to their graph through an assignment slot. After projection, every such occurrence has the uniform form `pr (fst x) (fst y) ∈ fst (lookup f γ)`, so the later single-valuedness and domain arguments can use one membership statement throughout.

```agda
  → (γ ⊨ appAt f x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (lookup f γ))
appAt-adequate f = appTerm-adequate (var f)
```

The graph being read need not sit in a variable slot; it may be a fixed element of the model named directly. The constant term `con F` is exactly that, and the adequacy statement simplifies accordingly: since the constant is interpreted as the element `F` itself, the right-hand side is membership in `fst F`, with no reference to the environment for the graph.

The definition instantiates the shared reader at `con F`. Because the constant is interpreted as itself, the bounded existential ranges directly over the members of `fst F`, and the adequacy statement records exactly that: satisfaction is a path to the membership of the projected pair of the two argument values in `fst F`. The membership on the right is ambient membership after projection; the existential on the left still quantifies over elements of the model.

```agda
appC : ∀ {n} → S → Fin n → Fin n → Formula S n
appC F = appTerm (con F)

appC-adequate : ∀ {n} (F : S) (x y : Fin n) (γ : S ^ n)
  → (γ ⊨ appC F x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F)
```

The proof is the shared adequacy theorem at the constant term, and needs no argument of its own. Together with `appAt`, the dictionary now recognizes pair membership in a graph given by a slot and in a graph given as a fixed element, each with its exact meaning as an ambient membership.

```agda
appC-adequate F = appTerm-adequate (con F)
```

## Single-valuedness

A graph is single-valued when any two pairs in it with the same first component have the same second component. This is a statement purely about membership of pairs; it neither says that the graph has any members at all nor that a given argument occurs in it, so it is logically independent of the domain condition that comes later.

The claim is stated as two directions rather than a single path, in the form in which it is actually consumed: reading outward, from the object-language assertion to an equation between the underlying sets of two values recorded against the same argument.

Read from the outside in: for all `x`, for all `y`, for all `y'`, if the pair of `x` and `y` belongs to the graph then, if the pair of `x` and `y'` also belongs, the values `y` and `y'` are equal. The equality demanded is between the underlying sets of the two values, since `y` and `y'` are themselves elements of the model. Nothing here says the graph is inhabited, or that every argument has a value; that is the separate domain condition.

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

The two directions are stated for a fixed graph slot `f` and a fixed environment `γ`, so a local predicate records the external meaning once. `Holds x y` says that the projected pair of `x` and `y` belongs to the underlying set of the graph; this is exactly the shape one application of `appAt-adequate` produces. The two adequacy instances that follow fix which of the two implications is being read: `at` for the pair with the value `y`, `at'` for the pair with `y'`.

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

    at : (x y y' : S)
```

Each helper is an instance of the application adequacy at the environment extended by the three quantified elements, which shifts the indices of the formula accordingly. Because `at` and `at'` are paths between propositions, a proof can be moved from either side to the other by transport; the two direction lemmas below do exactly this, in opposite orientations.

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

    at' : (x y y' : S)
```

Reading the object-language claim outward gives the usable conclusion. Given satisfaction of `svAt f`, the quantifiers supply the implication for arbitrary elements `x`, `y`, `y'` of the model; feeding it the two memberships `Holds x y` and `Holds x y'`, each first transported from its external form into the satisfaction the quantifiers expect, yields the equality `fst y ≡ fst y'` of the two underlying values. Note that the conclusion is an equality of projected sets, while the value equalities between `y` and `y'` as elements of the model are not claimed.

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

  svAt-out : ⟨ γ ⊨ svAt f ⟩
```

The converse builds satisfaction rather than extracting it. A function taking any three elements with two agreeing memberships to the equality of their values is exactly what the three quantifiers and the two implications ask for; each expected membership proof is manufactured by transporting the external one forward along `at` or `at'`. Together the two lemmas say that satisfaction of `svAt f` and the external single-valuedness condition imply each other, though the statement keeps them as two functions rather than one packaged path.

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

  svAt-in : ((x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y')
          → ⟨ γ ⊨ svAt f ⟩
```

The introduction direction `svAt-in` mirrors the extraction, with the transports pointing the other way: each external membership is carried forward along the adequacy path into the satisfaction the implications expect, and the three quantifiers then apply the function `h`. Both directions keep the whole statement at the level of underlying sets: the conclusion is an equality of the projected values `fst y` and `fst y'`, and the memberships supplied are about projected pairs. Nothing here asserts that every argument has a value, or that the graph is inhabited; those are separate questions settled by the domain condition.

```agda
  svAt-in h x y y' p q = h x y y'
    (subst ⟨_⟩ (at x y y') p) (subst ⟨_⟩ (at' x y y') q)
```

## The domain

The application reader already proved for the pair reader answers one question: does the pair of these two values belong to the graph? A graph can meet it at some arguments and miss at others, so the next structural property asks which arguments have entries at all. Being in the domain is simply having a value, and the reader for it is a single unbounded existential over the model. The domain condition then compares a candidate set `d` with the graph by saying that membership in `d` and having a value imply each other, stated as two implications because the object language has no biconditional of its own.

The three logical components developed so far, application, single-valuedness, and the exact domain, are independent of one another, and each is needed separately later: a graph can be single-valued yet miss arguments, defined exactly on `d` yet multi-valued, and so on. What the condition does not do is construct anything; it is a predicate that one candidate set either satisfies or fails. The two extraction lemmas are each used in one direction: `domAt-out` consumes an actual entry and yields domain membership, while `domAt-in` consumes domain membership and yields only the truncated existence of an entry, since from membership in the domain alone one merely knows that some entry exists. The introduction direction, needed when a set must be shown to satisfy the description from external evidence, carries a third name.

The definition is a single unbounded existential over the model: there merely exists a value `y` with the pair of the argument and `y` in the graph. The quantifier ranges over the carrier `S` of the model, not over a stage of the hierarchy, so the reader says exactly what it should. The adequacy statement unfolds the existential's satisfaction to the corresponding dependent sum; since `∃[ y ∶ S ] _` packages the existence of `y` propositionally, the right-hand side is itself truncated, asserting only that some such `y` exists.

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

inDomAt-adequate : ∀ {n} (f x : Fin n) (γ : S ^ n)
  → (γ ⊨ inDomAt f x)
  ≡ (∃[ y ∶ S ] (pr (fst (lookup x γ)) (fst y) ∈ fst (lookup f γ)))
```

The proof needs no new argument: satisfaction of an unbounded existential is the join of its fibers, so the two sides agree pointwise at each `y`, and the pointwise agreement is one instance of the application adequacy at the extended environment. With having a value settled, the domain condition `domAt f d` compares a candidate set `d` with the graph in both directions: for every element `x`, membership of the projected `x` in `d` implies having a value, and having a value implies membership in `d`. The two implications are conjoined because the language supplies no symbol standing for their joint claim.

```agda
inDomAt-adequate f x γ =
  cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ y → appAt-adequate (suc f) (suc x) zero (y ∷ γ)))

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

The direction lemmas are stated for a fixed graph slot `f`, a fixed candidate `d`, and a fixed environment `γ`. The helper `step` fixes once and for all the adequacy path for the quantified body: at an element `x` of the model, satisfaction of the having-a-value formula is a path to the truncated existence of a `y` with the projected pair of `x` and `y` in the graph. Every transport below goes through this one path.

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

The extraction `domAt-out` consumes an entry and yields domain membership. Given an actual witness pair `x`, `y` with the membership `p`, the truncated form is assembled as `∣ y , p ∣₁`, transported backward through `step` into the satisfaction the quantifier expects, and fed to the first implication at `x`. The output is a plain membership proof of the projected `x` in the projected `d`, with no truncation left.

```agda
    step x = inDomAt-adequate (suc f) zero (x ∷ γ)

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

The extraction `domAt-in` runs the other way, and keeps the truncation. Domain membership `m` is fed to the second implication, whose conclusion is the satisfaction of the having-a-value formula; transporting forward through `step` turns it into the truncated dependent sum. That truncated form is the correct statement: from membership in the domain alone one merely knows that some entry exists, not which one.

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

  domAt-intro : ((x : S)
                 → (⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩
```

The introduction direction packages the two implications pointwise. The hypothesis asks, for each `x`, a pair of functions: one from the truncated existence of an entry to membership in `d`, and one back. Since the target propositions are propositions, consuming a truncated sum here is legitimate, and the transports through `step` in each component mirror those of the two extraction lemmas.

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

The assembly is exactly the shape of the conjunction of implications under the universal quantifier: for each `x` a pair whose first component answers the first implication and whose second answers the second, each component adjusted by the transport in the direction its side requires. With this, a set claimed to be the domain can be certified to satisfy `domAt f d` from purely external evidence.

```agda
                  , (λ m → subst ⟨_⟩ (sym (step x)) (g x .snd m))
```

## The pair, inside the model

The adequacy statements so far have read formulas of the model outward, into ambient facts. The remaining task is the reverse: to build things inside the model whose projections are the ambient sets the readers talk about. Everything rests on one construction, the ordered pair of two elements of the model. It exists because the model has its own pairing operation, and applying it three times following the Kuratowski scheme produces an internal pair of any two elements, with no certificate to supply, since the pairing lands in the carrier by construction. What must be proved is that this internal pair projects to the ambient one: reading it through the underlying set gives exactly the hierarchy's pair of the projected components, with the singleton identity handling the component that appears twice.

The Kuratowski coding inside the model mirrors the ambient definition term by term: `pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆` becomes `pairʟ` applied to `pairʟ a a` and `pairʟ a b`. Because `pairʟ` lands in the carrier `S` by construction, the result is an element of the model with no certificate to supply: each inner occurrence of `pairʟ` already carries its own constructibility internally, so composing them needs no additional proof.

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

prʟ-fst : (a b : S) → fst (prʟ a b) ≡ pr (fst a) (fst b)
prʟ-fst a b =
    pairʟ-fst (pairʟ a a) (pairʟ a b)
```

The projection equation unfolds the same recursion in `V`. The outer projection gives the pair of the two projections; the first component projects to the unordered pair of `fst a` with itself, which the hierarchy's identity `pair-singleton` collapses to the singleton of `fst a`. The result is the promised identification: reading the model's pair through the underlying set yields exactly `pr (fst a) (fst b)`. This equation is the hinge of the next section, since every tag-and-pair code will be projected through it.

```agda
  ∙ cong₂ ⁅_,_⁆ (pairʟ-fst a a ∙ pair-singleton (fst a)) (pairʟ-fst a b)
```

## The coding, at the model

The pair `prʟ` and the numerals are injective, which is what the generic coding scheme asks of a structure, so terms and formulas now code into `L` itself. Two facts follow. A code is an element of the model **by construction**, with no constructibility certificate to supply; and distinct expressions have distinct codes, which is what a table indexed by codes needs, since two different subformula occurrences must not share a key.

The bridge then compares the two codings. Internal pairing and numerals project to their ambient counterparts, so every code, being built from tags pairing a numeral with a payload, projects to the ambient code of the formula whose constants have been projected by `fst`. This is what lets the adequacy theorems proved on the hierarchy side be applied to codes built inside the model.

Injectivity of `prʟ` follows the same route as its projection: if the pairs of model elements are equal, projecting both sides along `prʟ-fst` gives equality of the ambient pairs, and the ambient injectivity `pr-inj` recovers equality of the projected components. Each component equality lives in a dependent sum whose second component is a proposition, namely the certificate `isL`, so `Σ≡Prop` licenses concluding the full equality of the model elements from the equality of their first components.

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

The path of ambient pair equalities is assembled from the three available equations: reverse the projection of the left pair, apply the assumed equality under `fst`, and project the right pair. The same pattern gives injectivity of the numerals, where `numeralL-fst` plays the projection role and `#-inj′` recovers equality of the natural number indices from equality of the projected finite ordinals.

```agda
  q : pr (fst a) (fst b) ≡ pr (fst c) (fst d)
  q = sym (prʟ-fst a b) ∙ cong fst e ∙ prʟ-fst c d

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

With the two injectivities in hand, the generic coding scheme instantiates at the structure `𝒮ʟ` with `prʟ` and `numeralL` as its pairing and numerals: the resulting module `LCode` codes terms and formulas into the carrier `S`. The bridge lemmas then relate the two codings, and the basic case is already visible in `tagBridge`: a tag pairs a numeral with a payload, so its projection is the ambient tag of the projected payload, by `prʟ-fst` and the projection equation of the numeral.

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

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

codeBridgeTm : ∀ {n} (t : Term S n) → fst LCode.⌜ t ⌝ᵗ ≡ VCode.⌜ mapTm fst t ⌝ᵗ
codeBridgeTm (con c) = tagBridge 0 c
```

For terms the recursion has two cases. A constant is coded as the tag 0 applied to itself, so the bridge is `tagBridge 0` at that constant. A variable is coded as the tag 1 applied to the numeral of its index, and the extra congruence step moves the projection equation of that numeral under the tag, since `mapTm fst` has replaced the variable constant by its projection. The formula recursion starts the same way: membership pairs its two terms, with the tag 0 here marking the membership constructor of the ambient coding, and the payload path is `prʟ-fst` followed by congruence over the two term bridges.

```agda
codeBridgeTm (var i) =
  tagBridge 1 (numeralL (toℕ i)) ∙ cong (VCode.mkTag 1) (numeralL-fst (toℕ i))

codeBridge : ∀ {n} (φ : Formula S n) → fst LCode.⌜ φ ⌝ ≡ VCode.⌜ mapFo fst φ ⌝
codeBridge (t ∈̇ u) = tagBridge 0 _ ∙ cong (VCode.mkTag 0)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
```

The remaining binary constructors repeat one pattern. Each is marked by its own tag, the payload is the ordered pair of the codes of the two immediate subformulas, and the projection path is one tag equation composed with congruence over the pair of the two recursive bridges. Equality, conjunction, disjunction, and implication differ only in the tag number and in which subformula bridge is applied where.

```agda
codeBridge (t ≐ u) = tagBridge 1 _ ∙ cong (VCode.mkTag 1)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (a ∧̇ b) = tagBridge 2 _ ∙ cong (VCode.mkTag 2)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ∨̇ b) = tagBridge 3 _ ∙ cong (VCode.mkTag 3)
```

The nullary and unary constructors fit the same frame with degenerate payloads. Falsity is coded as the tag 5 applied to the numeral of zero, so its bridge is one tag equation with the numeral projection inside. The unbounded quantifiers carry a single subformula, so no pairing occurs and the payload path is just the recursive bridge of the body, transported under the tag.

```agda
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ⇒̇ b) = tagBridge 4 _ ∙ cong (VCode.mkTag 4)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge ⊥̇       = tagBridge 5 _ ∙ cong (VCode.mkTag 5) (numeralL-fst 0)
codeBridge (∃̇ a)   = tagBridge 6 _ ∙ cong (VCode.mkTag 6) (codeBridge a)
```

The bounded quantifiers are the only constructors mixing both levels: a bounded quantifier pairs a term with a formula, so the payload path projects the outer pair and then applies the term bridge and the formula bridge to the two components. With this, the recursion covers every constructor of terms and formulas, and every internal code is known to project to the ambient code of the projected formula.

```agda
codeBridge (∀̇ a)   = tagBridge 7 _ ∙ cong (VCode.mkTag 7) (codeBridge a)
codeBridge (∀̇∈ t a) = tagBridge 8 _ ∙ cong (VCode.mkTag 8)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
codeBridge (∃̇∈ t a) = tagBridge 9 _ ∙ cong (VCode.mkTag 9)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
```

## Environments

An environment over a set B is a function whose values all lie in B, so a candidate set e qualifies as one exactly when four things hold at once: it is single-valued, its domain is the given set d, its values lie in B, and it is *made of pairs*. The four clauses are logically independent, and each earns its place. Single-valuedness constrains only arguments that appear twice; the domain clause says that the arguments with entries are exactly the members of d; the value restriction says that every value lies in B. The first three speak only about members of e that are ordered pairs, so a set carrying additional non-pair elements would still pass all of them. The fourth conjunct closes this by requiring every member of e to be a pair of a member of d and a member of B, which makes each environment a subset of d × B; that exclusion of non-pair members is what the first three cannot supply.

What this section provides is a predicate on a single candidate, together with extraction lemmas that read each conjunct back out. Whether some particular set *is* the set of all environments of a given length is a different and harder question, not settled here.

The third conjunct restricts the values. Its statement quantifies over two variables x and y and says: whenever the pair of x and y belongs to the graph e, the value y must belong to B. Note what is *not* said: nothing requires any particular x to have a value at all, that is the separate domain clause. The clause constrains only existing entries, so it neither makes the graph a function nor fixes its domain.

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

valuesInAt-out : ∀ {n} (f B : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ valuesInAt f B ⟩ → (x y : S)
```

Reading the clause out is one direction, and it is direct. Given a pair with first component x and value y in the graph, apply the universal quantifiers at x and y; the remaining obligation is the implication inside. The membership fact p is first converted into a satisfaction of the antecedent, which `appAt-adequate` identifies with membership at the projected environment (y ∷ x ∷ γ), so transporting along the symmetric equation supplies exactly the argument the quantified body demands. The conclusion is membership of the projected value in the projected B, no truncation involved anywhere.

```agda
               → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
               → ⟨ fst y ∈ fst (lookup B γ) ⟩
valuesInAt-out f B γ h x y p = h x y
  (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ))) p)

pairsInAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
```

The fourth conjunct, the pairs clause, is written with bounded quantifiers alone. It says: for every member s of e there is a member u of d and a member v of B with s equal to the pair of u and v. Because the quantifiers range over actual members, the clause constrains only what already lies in the sets e, d and B, and its meaning will be read off those sets after projection. The body is the pair reader `prAtL` from earlier in this chapter, at indices shifted by the three binders.

```agda
pairsInAt e d B =
  ∀̇∈ (var e) (∃̇∈ (var (suc d)) (∃̇∈ (var (suc (suc B)))
    (prAtL (suc (suc zero)) (suc zero) zero)))

pairsIn-out : ∀ {n} (e d B : Fin n) (γ : S ^ n) → ⟨ γ ⊨ pairsInAt e d B ⟩
            → (s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
```

The extraction from the pairs clause keeps the shape of satisfaction: the conclusion is a propositional truncation, merely asserting that such u and v exist. The hypothesis h is an ordinary proof that the formula holds, and s∈ is an ordinary membership of the projected s in the projected e. The type says precisely what is recovered: u in d, v in B, and the underlying set of s equal to the pair of their underlying sets, all merely.

```agda
            → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                  (⟨ fst u ∈ fst (lookup d γ) ⟩
                   × (⟨ fst v ∈ fst (lookup B γ) ⟩
                      × (fst s ≡ pr (fst u) (fst v)))))) ∥₁
pairsIn-out e d B γ h s s∈ = PT.rec squash₁
```

The proof peels the two bounded existentials inside the truncation. Elimination of propositional truncation is legitimate here because the target is again a proposition, the truncation of a Sigma type, so nothing is chosen globally: each branch transforms its own witnesses. The inner step is the same transport seen throughout this chapter: `prAtL-adequate` turns the body's satisfaction into the path `fst s ≡ pr (fst u) (fst v)`, with the environment extended by v, u, s in binder order.

```agda
  (λ { (u , (u∈ , hv)) → PT.map
    (λ { (v , (v∈ , hp)) → u , (v , (u∈ , (v∈ , subst ⟨_⟩
      (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ)) hp))) })
    hv })
  (h s s∈)
```

The reverse direction takes the per-member statement as a hypothesis. For every s whose projection lies in the projected e, the hypothesis merely supplies a truncated quadruple: u and v, their memberships, and the pair equation; the task is to turn that into satisfaction of the bounded formula. The two directions are kept as separate lemmas rather than merged into a path, because later arguments use exactly one direction at a time.

```agda
pairsIn-in : ∀ {n} (e d B : Fin n) (γ : S ^ n)
           → ((s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
              → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                    (⟨ fst u ∈ fst (lookup d γ) ⟩
                     × (⟨ fst v ∈ fst (lookup B γ) ⟩
```

The construction transforms the truncated data of the hypothesis directly into satisfaction of the formula. The witnesses u and v pass through with their memberships, and the pair equation eq is carried to the body's satisfaction by transporting along the symmetry of the adequacy path, since here one travels from the set-level pair equation back to the reader's satisfaction. Truncation enters only through `PT.map`, which rebuilds the truncated sum around the rearranged data; the formula's own meaning supplies whatever truncation its quantifiers carry.

```agda
                        × (fst s ≡ pr (fst u) (fst v)))))) ∥₁)
           → ⟨ γ ⊨ pairsInAt e d B ⟩
pairsIn-in e d B γ k s s∈ = PT.map
  (λ { (u , (v , (u∈ , (v∈ , eq)))) → u , (u∈ , ∣ v , (v∈ , subst ⟨_⟩
    (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ))) eq) ∣₁) })
```

Assembling the four clauses gives the definition of being an environment over d with values in B: single-valuedness, the exact domain, the value restriction, and the pairs clause, conjoined with `∧̇`. An anonymous module then fixes the arity, the three indices, an environment γ, and a proof that γ satisfies the conjunction, so the four projections can be stated once and used without repeating these parameters.

```agda
  (k s s∈)

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

module _ {n : ℕ} (e d B : Fin n) (γ : S ^ n) (h : ⟨ γ ⊨ envOverAt e d B ⟩) where
```

Each projection is just the corresponding component of the nested pair that the satisfaction of a fourfold conjunction is. The first is single-valuedness of e, the second the domain clause relating e and d, the third the value restriction toward B, and the fourth the pairs clause itself. With these in hand, an argument that needs only one aspect of environment-hood can take it without rebuilding the conjunction, and an argument that constructs an environment can be checked conjunct by conjunct.

```agda
  envOver-sv     : ⟨ γ ⊨ svAt e ⟩
  envOver-sv     = h .fst
  envOver-dom    : ⟨ γ ⊨ domAt e d ⟩
  envOver-dom    = h .snd .fst
  envOver-values : ⟨ γ ⊨ valuesInAt e B ⟩
```

The four projections also expose why the definition is modular: uniqueness, domain, range, and pair shape can be transported or used independently, while their conjunction remains the single assertion that the candidate is an environment over `d` into `B`.

```agda
  envOver-values = h .snd .snd .fst
  envOver-pairs  : ⟨ γ ⊨ pairsInAt e d B ⟩
  envOver-pairs  = h .snd .snd .snd
```

Every reader built so far inspects only the underlying sets that the assignment places at its indices: a satisfaction claim about a graph, a domain, or a value set is always stated after projecting the looked-up entries by `fst`. It follows that the description of an environment depends extensionally on just three sets, the projected graph, the projected domain, and the projected value set, and on nothing else about the assignment. So if two assignments, possibly of different arities, place the same three sets at the indices the description consults, the description holds at one exactly when it holds at the other.

This is what will later let a statement about an assignment be turned into a statement about a set that a construction actually built: the construction is free to present its environments through any indexing it likes, and as long as the three underlying sets match, the description carries over unchanged.

The transfer theorem needs the introduction direction of the value restriction, the direction not extracted earlier: from the statement about every pair in the graph, back to a satisfaction. Given a function sending any pair in the graph to a value in B, the two universal quantifiers are applied, and the membership fact is converted into a satisfaction of the antecedent by the adequacy equation of the application reader. With this, both directions of `valuesInAt` are available as lemmas, one each.

```agda
valuesInAt-in : ∀ {n} (f B : Fin n) (γ : S ^ n)
              → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
                 → ⟨ fst y ∈ fst (lookup B γ) ⟩)
              → ⟨ γ ⊨ valuesInAt f B ⟩
valuesInAt-in f B γ k x y hp = k x y
```

The theorem compares two assignments γ and γ', possibly of different arities, with three indices chosen on each side. The hypotheses are paths between the projected sets: the graph, the domain, and the value set are equal as sets of the hierarchy, element by element. Nothing is assumed about how the indices on the two sides relate, only about what the lookups return after projection; this is exactly the situation of a construction that re-indexes its environments.

```agda
  (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ)) hp)

envOverAt-transport : ∀ {n n'} (γ : S ^ n) (γ' : S ^ n')
                      (e d B : Fin n) (e' d' B' : Fin n')
                    → fst (lookup e γ) ≡ fst (lookup e' γ')
                    → fst (lookup d γ) ≡ fst (lookup d' γ')
```

Single-valuedness transfers by composing the extraction lemma at γ with the introduction lemma at γ'. Given two values y and y' recorded against x at γ', the hypothesis is first moved back to a satisfaction at γ along the path that identifies pair membership in the projected graph on the two sides; the extraction lemma then yields equality of the two projected values, and the introduction lemma repackages it as satisfaction at γ'. The equality itself needs no transport, since values are elements of S on both sides.

```agda
                    → fst (lookup B γ) ≡ fst (lookup B' γ')
                    → ⟨ γ ⊨ envOverAt e d B ⟩ → ⟨ γ' ⊨ envOverAt e' d' B' ⟩
envOverAt-transport γ γ' e d B e' d' B' qe qd qb h =
    svAt-in e' γ' (λ x y y' p q →
      svAt-out e γ (envOver-sv e d B γ h) x y y'
```

The domain clause transfers through the introduction lemma for `domAt`, supplying both implications at γ'. The first implication reads: having a value forces membership in the domain. From the merely truncated existence of a value, the extraction lemma at γ produces membership in the projected domain d, which needs no witness to be eliminated into, and the path qd carries that membership across to d'.

```agda
        (subst ⟨_⟩ (sym (at x y)) p) (subst ⟨_⟩ (sym (at x y')) q))
  , ( domAt-intro e' d' γ'
      (λ x → (λ m → subst (λ w → ⟨ fst x ∈ w ⟩) qd
                (PT.rec (snd (fst x ∈ fst (lookup d γ)))
                  (λ { (y , p) → domAt-out e d γ (envOver-dom e d B γ h) x y
```

The second implication reads in the opposite direction: membership in the domain forces having a value. A membership in d' is first moved back along the symmetric path, the extraction lemma at γ then yields the merely truncated existence of an entry, and the truncation is transformed internally by replacing the body's satisfaction with its γ'-side form. The value y itself passes through untouched, which is correct: the two graphs agree only after projection, and the entries are elements of S.

```agda
                         (subst ⟨_⟩ (sym (at x y)) p) })
                  m))
            , (λ hx → PT.map (λ { (y , p) → y , subst ⟨_⟩ (at x y) p })
                (domAt-in e d γ (envOver-dom e d B γ h) x
                  (subst (λ w → ⟨ fst x ∈ w ⟩) (sym qd) hx))))
```

For the value restriction, begin with a pair membership in the new projected graph. The symmetric graph-membership path moves it to the old graph; `valuesInAt-out` there yields membership of the value in the old set `B`; one forward transport along `qb : B ≡ B′` then gives membership in `B′`. Thus `qb` is used once, in the direction from the old value set to the new one.

```agda
    , ( valuesInAt-in e' B' γ'
        (λ x y p → subst (λ w → ⟨ fst y ∈ w ⟩) qb
          (valuesInAt-out e B γ (envOver-values e d B γ h) x y
            (subst ⟨_⟩ (sym (at x y)) p)))
      , pairsIn-in e' d' B' γ'
```

The pairs clause is the last to move, and the transports stay inside the truncation. Reading the clause out at γ gives, merely, witnesses u and v with their memberships in the projected d and B and the pair equation. The two memberships are carried to d' and B' by qd and qb respectively, while the equation `fst s ≡ pr (fst u) (fst v)` needs no transport at all: it speaks about underlying sets, and the hypotheses say exactly that those agree, so it is the same equation on both sides.

```agda
        (λ s s∈ → PT.map
          (λ { (u , (v , (u∈ , (v∈ , eq)))) →
            u , (v , ( subst (λ w → ⟨ fst u ∈ w ⟩) qd u∈
                     , ( subst (λ w → ⟨ fst v ∈ w ⟩) qb v∈ , eq ) )) })
          (pairsIn-out e d B γ (envOver-pairs e d B γ h) s
```

The remaining ingredient is the path `at`: for each x and y, the path identifying membership of the pair in the projected graph on the two sides. It is congruence, applying the equality qe of the two graphs to the membership predicate at fixed pair components. Every transport inside the theorem that concerns the graph goes through this one path, so the whole argument rests on the three given equalities and nothing hidden.

```agda
            (subst (λ w → ⟨ fst s ∈ w ⟩) (sym qe) s∈))) ) )
  where
  at : (x y : S) → (pr (fst x) (fst y) ∈ fst (lookup e γ))
                 ≡ (pr (fst x) (fst y) ∈ fst (lookup e' γ'))
  at x y = cong (λ w → pr (fst x) (fst y) ∈ w) qe
```

## A container for pair components

Reading a pair-shaped code exposes its two components, and it is convenient to have both available as members of a single constructible set. The candidate is forced by the mathematics: if `fst x` is the ordered pair of `fst u` and `fst v`, then the unordered pair `⁅ fst u , fst v ⁆` is a member of `fst x`, hence itself constructible by transitivity of `L`, and both components are members of it. The section records exactly this witness together with the three membership facts, as a type `Container x u v` and a construction `container` producing it from the path `fst x ≡ pr (fst u) (fst v)`.

The type packages one element `s` of the model with three ambient membership facts, all stated after projection: the underlying set of `s` is a member of `fst x`, and the underlying sets of `u` and `v` are members of `fst s`. No claim is made beyond these; in particular nothing asserts that `s` is the least such set. The construction `container` takes the hypothesis that `fst x` equals `pr (fst u) (fst v)` and returns the witness with its three certificates in one package.

```agda
Container : (x u v : S) → Type (ℓ-suc ℓ)
Container x u v = Σ[ s ∈ S ] (⟨ fst s ∈ fst x ⟩ × (⟨ fst u ∈ fst s ⟩ × ⟨ fst v ∈ fst s ⟩))

opaque
  container : (x u v : S) → fst x ≡ pr (fst u) (fst v) → Container x u v
  container x u v e = s , (s∈ , (∈pair-introL refl , ∈pair-introR refl))
```

The witness is the unordered pair of the two underlying sets. As one member of the outer unordered pair in the Kuratowski encoding, it belongs to `pr (fst u) (fst v)` by the introduction rule at the reflexive path, and transporting along the hypothesis `e` moves that membership into membership in `fst x`. This is precisely the input transitivity of `L` consumes: since the unordered pair is a member of a constructible set, `isL-trans` yields it as an element of `S`, certificate included. The two remaining memberships, of `fst u` and `fst v` in it, are the two introduction rules at reflexive paths.

```agda
    where
    s∈ : ⟨ ⁅ fst u , fst v ⁆ ∈ fst x ⟩
    s∈ = subst (λ w → ⟨ ⁅ fst u , fst v ⁆ ∈ w ⟩) (sym e) (∈pair-introR refl)
    s : S
    s = ⁅ fst u , fst v ⁆ , isL-trans s∈ (snd x)
```

## Recap

The chapter closes the gap between the two sides of the semantics. Formulas are satisfied in `L`, at environments of constructible elements, while the concrete facts they need to express are ambient facts about underlying sets; the dictionary entries connect the two by exact adequacy paths. Ordered pair recognition is absolute, graph membership acquires a constructible witness through transitivity, and the environment description collects single-valuedness, exact domain, value restriction, and the pairs clause, depending only on the three projected sets. Syntax coding then instantiates inside `L` itself, and the bridge shows that internal codes project to the ambient codes of the projected formulas, so the hierarchy-side readers apply to internally built codes. The container supplies, for a pair-shaped code, one constructible set holding both components.