BedrockCoding formulas over the constructible model
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapAn 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
∙ 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.
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.
≡ (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.
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.
(λ { (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.
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.
→ (γ ⊨ 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.
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.
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.
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'.
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.
→ ((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.
→ ((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.
→ (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.
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.
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.
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.
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.
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.
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.
→ ⟨ 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.
, (λ 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.
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.
∙ 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.
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.
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.
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.
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.
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.
(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.
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.
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.
→ ⟨ 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.
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.
→ ∥ (Σ[ 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.
(λ { (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.
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.
× (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.
(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.
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.
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.
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.
(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.
→ 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'.
(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.
(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.
, ( 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.
(λ 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.
(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.
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.
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.