--- title: "Formulas for singletons and pairs" module: L.Coding.PairFormulas lang: en site: "Bedrock" description: "Formulas for singletons and pairs" stage: "Internal coding: expressions and domains" reading_order: 40 canonical: https://bedrock.institute/en/L.Coding.PairFormulas.html html: L.Coding.PairFormulas.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/PairFormulas.lagda.md prerequisites: [Base.Prelude, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy, V.Coding] routes: [internal-satisfaction] translations: [https://bedrock.institute/zh/L.Coding.PairFormulas.md, https://bedrock.institute/ja/L.Coding.PairFormulas.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Formulas for singletons and pairs The goal of this chapter is to let the object language recognize that one assigned set is the Kuratowski ordered pair of two others, and, along the way, to recognize singletons and unordered pairs, of which the Kuratowski pair is built. A first-order formula can speak only of membership and equality, so recognition must be extensional: a set is recognized as `pr U W` by saying, through membership alone, exactly which members it has. Three bounded formulas are constructed: `sglAt` says "this set is the singleton of that one", `pairAt` says "this is the unordered pair of those two", and `prAt` combines these into "this is the Kuratowski pair of those two". The adequacy theorem at the end is an exact identification. For any environment, satisfaction of `prAt q u v` is a path of truth values to the proposition that the value at position `q` equals `pr` applied to the values at `u` and `v`. Nothing weaker, such as a one-way implication, is claimed. Because the quantifiers of each formula are bounded by an assigned set and its free-variable positions are de Bruijn indices given as arguments, the same formula works at any depth of nesting. Every clause is an atom or a bounded quantifier, so each reader is Δ₀ in the Lévy hierarchy. The external target has a specific membership shape: `pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`. Its outer set is an unordered pair whose first member is the singleton of `U` and whose second member is the unordered pair of `U` and `W`. Recognizing the ordered pair therefore reduces to three conditions: the two required members occur, and every member is one of them. The last condition is propositionally truncated, matching the classification of unordered-pair membership; it records the alternative without choosing a side. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Coding.PairFormulas {ℓ : Level} where open import FOL.Syntax ``` The tool for expressing the descriptions is the bounded fragment of the first-order language. Its atoms `_∈̇_` and `_≐_` and its connectives `_∧̇_` and `_∨̇_` state membership and equality between the sets assigned to positions; its quantifiers `∀̇∈` and `∃̇∈` are always bounded by an assigned set. Formulas built from these alone form the class `Δ₀` of the Lévy hierarchy, checked syntactically by `checkΔ₀`. The target of recognition is the Kuratowski coding `pr`, defined by `pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`: an ordered pair is presented as an unordered pair of two sets, the singleton of `U` and the pair of `U` and `W`. The recognition problem thus reduces to saying, with bounded formulas, that a set has a member which is the singleton of `U`, a member which is the unordered pair of `U` and `W`, and no other members. Singleton and unordered-pair membership have their own classifications, and extensionality will convert complete membership conditions into equalities of sets. ```agda using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ ) import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) open import V.Coding {ℓ} using ( pr ) ``` Singleton and unordered-pair membership are supplied in two equivalent forms: hierarchy membership `⟨ y ∈ b ⟩` and the small classified membership used by their constructions. The equivalence `∈∈ₛ` passes between them. For a singleton, the classification yields the path `y ≡ u`; for an unordered pair, it yields the truncated alternative `∥ (y ≡ u) ⊎ (y ≡ v) ∥₁`. Once these membership descriptions are proved in both directions, `⇔toPath` turns each equivalence of membership propositions into the path required by extensionality. ```agda open import Cubical.Data.Unit using ( tt ) import Cubical.Data.Sum as Sum open Sum using ( _⊎_; inl; inr ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁ ) ``` The semantics takes its truth values in `hProp` at level `ℓ-suc ℓ`. A formula does not evaluate to a bare boolean: its value is a proposition, and satisfaction of a formula under an environment is itself a proposition rather than a decision. Conjunction and disjunction act directly on these `hProp` truth values when reading compound formulas. This propositional setting matters for the goal: it allows satisfaction of a bounded formula to be identified, path-for-path, with an external condition such as equality of a set with its coded pair. ```agda open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ ) open import Cubical.HITs.CumulativeHierarchy.Constructions ``` Within this semantics, the constant interpretation is fixed to be the identity on `V ℓ`: a constant of the language is simply a set, denoting itself. Consequently `⟦ var k ⟧ γ` is the value that the environment `γ` assigns to position `k`, and a formula may speak directly about the assigned sets. ```agda using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( SetPackage ) -- lint-agda: keep (used qualified: SetPackage.classification) open InfinitySet using ( #_ ) ``` This is what makes the adequacy statement below meaningful: satisfaction of the reader `prAt` at positions `q`, `u`, `v` will be compared, as truth values, with the equality of `⟦ var q ⟧ γ` and `pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)`. ```agda module Sem = FOL.Semantics 𝒮ᵥ open Sem using ( _^_ ) open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ ) ``` ## Singletons and pairs, characterized A set whose only member is `u` is the singleton of `u`, and a set whose members are exactly `u` and `v` is their unordered pair. These are the external meanings that the object-language readers will express, so they are proved here once, at the meta level. Both characterizations rest on the same move: if two sets admit the same members, extensionality `extensionalV` turns the pointwise membership equivalence into a path of sets. The two directions differ in strength. That a member of `⁅ u ⁆s` equals `u` is a path without an outer truncation; that a member of `⁅ u , v ⁆` is one of `u` and `v` is merely so, a propositionally truncated disjunction. The proofs keep this distinction exact. Membership in a singleton is completely described by the classification of `SingletonPackage`: `y` belongs to `⁅ u ⁆s` precisely when `y` equals `u`. The bridge `∈∈ₛ` moves between the ambient membership of the hierarchy and this small membership, so `∈sgl-elim` chains the bridge's forward leg with the classification to extract an actual path `y ≡ u` from a mere membership proof, and `∈sgl-intro` runs the same two steps backwards. No truncation is involved: the equality path is available directly and, since `V ℓ` is an h-set, remains a proposition. ```agda ∈sgl-elim : {u y : V ℓ} → ⟨ y ∈ ⁅ u ⁆s ⟩ → y ≡ u ∈sgl-elim {u} {y} h = SetPackage.classification (SingletonPackage u) y .fst (∈∈ₛ {a = y} {b = ⁅ u ⁆s} .fst h) ∈sgl-intro : {u y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u ⁆s ⟩ ∈sgl-intro {u} {y} e = ∈∈ₛ {a = y} {b = ⁅ u ⁆s} .snd ``` For the unordered pair, the classification `pairing-ax` describes membership by a disjunction: a member equals `u` or it equals `v`. Here the truncation appears. `∈pair-elim` converts a membership proof into a merely-disjunct statement `∥ (y ≡ u) ⊎ (y ≡ v) ∥₁`, because the underlying classification returns a propositionally truncated choice of side, and eliminating it into the untruncated sum is not allowed. Conversely, `∈pair-introL` and `∈pair-introR` each take an explicit path on one side and seal it as merely one side or the other, obtaining membership. ```agda (SetPackage.classification (SingletonPackage u) y .snd e) ∈pair-elim : {u v y : V ℓ} → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁ ∈pair-elim {u} {v} {y} h = pairing-ax u v y .fst (∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .fst h) ∈pair-introL : {u v y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u , v ⁆ ⟩ ∈pair-introL {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd ``` The second introduction is symmetric to the first. With membership into and out of both constructions available, the external characterizations can be stated. `sgl-char` says: if `u` belongs to `x` and every member of `x` equals `u`, then `x` is the singleton of `u`. `pair-char` says the analogous thing for two components, with the every-member clause now merely disjunctive. Both conclusions are paths of sets, and both will later supply exactly the clauses that the reader `prAt` expresses. ```agda (pairing-ax u v y .snd ∣ inl e ∣₁) ∈pair-introR : {u v y : V ℓ} → y ≡ v → ⟨ y ∈ ⁅ u , v ⁆ ⟩ ∈pair-introR {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd (pairing-ax u v y .snd ∣ inr e ∣₁) sgl-char : (x u : V ℓ) → ⟨ u ∈ x ⟩ → ((y : V ℓ) → ⟨ y ∈ x ⟩ → y ≡ u) → x ≡ ⁅ u ⁆s ``` To prove `x ≡ ⁅ u ⁆s` from the two membership hypotheses, extensionality is applied pointwise: for each `y`, the proposition `⟨ y ∈ x ⟩` must be connected to `⟨ y ∈ ⁅ u ⁆s ⟩` by a path, and `⇔toPath` builds exactly such a path from an iff. The forward direction uses the hypothesis that all members of `x` equal `u` and then reintroduces membership in the singleton; this is `sub₁`. ```agda sgl-char x u hu hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y)) where sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u ⁆s ⟩ sub₁ y hy = ∈sgl-intro (hall y hy) sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u ⁆s ⟩ → ⟨ y ∈ x ⟩ ``` The backward direction `sub₂` starts from membership in the singleton and must produce membership in `x`. Elimination gives the path `y ≡ u`, and membership is then transported along its reversal: if `u` belongs to `x` and `y` is a path away from `u`, `y` belongs to `x` as well. This transport-along-a-path pattern is the standard substitute for comparing constructions directly, and it recurs in every remaining proof of the chapter. With both directions in place, `⇔toPath` assembles the pointwise equivalence and `extensionalV` returns the path `x ≡ ⁅ u ⁆s`. ```agda sub₂ y hy = subst (λ z → ⟨ z ∈ x ⟩) (sym (∈sgl-elim hy)) hu pair-char : (x u v : V ℓ) → ⟨ u ∈ x ⟩ → ⟨ v ∈ x ⟩ → ((y : V ℓ) → ⟨ y ∈ x ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁) → x ≡ ⁅ u , v ⁆ pair-char x u v hu hv hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y)) ``` The proof of `pair-char` follows the same plan, with one new feature: the every-member hypothesis is truncated, so the forward direction `sub₁` cannot pattern-match on which side `y` is on. Instead it eliminates the truncation `PT.rec` into the membership proposition `⟨ y ∈ ⁅ u , v ⁆ ⟩`, which is indeed proposition-valued, and dispatches on the two sides of the sum: a member equal to `u` enters the pair from the left, one equal to `v` from the right. This is the sanctioned way to use a merely-disjunct fact. ```agda where sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u , v ⁆ ⟩ sub₁ y hy = PT.rec ((y ∈ ⁅ u , v ⁆) .snd) (Sum.rec (∈pair-introL {u = u} {v = v}) (∈pair-introR {u = u} {v = v})) (hall y hy) sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ⟨ y ∈ x ⟩ ``` The backward direction `sub₂` mirrors this: from membership in `⁅ u , v ⁆` it obtains the truncated disjunction via `∈pair-elim`, eliminates it into the membership proposition `⟨ y ∈ x ⟩`, and in each branch transports the corresponding hypothesis `hu` or `hv` backward along the recovered path. Both `sub₁` and `sub₂` thus manufacture membership in `x` out of nothing more than the classification of the pair construction, and `extensionalV` upgrades the pointwise result to `x ≡ ⁅ u , v ⁆`. ```agda sub₂ y hy = PT.rec ((y ∈ x) .snd) (Sum.rec (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hu) (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hv)) (∈pair-elim hy) ``` ## The Kuratowski pair, at the meta level The reader `prAt` will say of a set `Q` that it contains a member which is the singleton of `U`, a member which is the unordered pair of `U` and `W`, and that every member is one of these two. This section proves that exactly these three conditions force `Q` to equal the Kuratowski pair `pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`, and conversely. The two auxiliary predicates below record the conditions one clause at a time, in precisely the shape that the satisfaction of a bounded formula will unfold to; the semantic lemmas of the adequacy section can then hand their hypotheses straight to the metalevel lemmas proved here, instead of proving anything a second time. The first predicate `SglOf U w` states that `w` is the singleton of `U` in purely membership terms: `U` belongs to `w`, and any `z` belonging to `w` equals `U` outright. The second, `PairOf U W w`, states that `w` is the unordered pair: both `U` and `W` belong to `w`, and every member is merely one of the two, a propositionally truncated disjunction. Both live at the level `ℓ-suc ℓ` because quantifying over all sets of `V ℓ` costs one level, the same level at which the semantics takes its truth values. ```agda private SglOf : V ℓ → V ℓ → Type (ℓ-suc ℓ) SglOf U w = ⟨ U ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ U) PairOf : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ) PairOf U W w = ``` The packages connect to equality through the characterizations of the previous section. If `w` carries `SglOf U`, its two components are exactly the hypotheses of `sgl-char`, which returns the path `w ≡ ⁅ U ⁆s`; similarly `pair-char` turns a `PairOf` package into `w ≡ ⁅ U , W ⁆`. Thus a package is a certificate of equality with the corresponding construction, and it is obtained without inspecting how `w` was built. ```agda ⟨ U ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ U) ⊎ (z ≡ W) ∥₁)) sglOf→≡ : {U w : V ℓ} → SglOf U w → w ≡ ⁅ U ⁆s sglOf→≡ {U} {w} (hu , hall) = sgl-char w U hu hall pairOf→≡ : {U W w : V ℓ} → PairOf U W w → w ≡ ⁅ U , W ⁆ pairOf→≡ {U} {W} {w} (hu , hv , hall) = pair-char w U W hu hv hall ``` The converse data also exists: the constructions themselves carry their own packages. For `⁅ U ⁆s`, membership of `U` follows from `∈sgl-intro` at the reflexive path, and every member equals `U` by `∈sgl-elim`; the unordered pair is packaged the same way using both introductions and `∈pair-elim`. Finally, since a package is a proposition-valued type in the set `w`, it can be transported along a path between sets: from `w ≡ ⁅ U ⁆s` one obtains `SglOf U w` by transporting the package of `⁅ U ⁆s` backward along the path. ```agda sglOf⁅⁆ : (U : V ℓ) → SglOf U ⁅ U ⁆s sglOf⁅⁆ U = ∈sgl-intro refl , (λ z z∈ → ∈sgl-elim z∈) pairOf⁅⁆ : (U W : V ℓ) → PairOf U W ⁅ U , W ⁆ pairOf⁅⁆ U W = ∈pair-introL refl , ∈pair-introR refl , (λ z z∈ → ∈pair-elim z∈) sglOf-subst : {U w : V ℓ} → w ≡ ⁅ U ⁆s → SglOf U w ``` With the packages in place, the metalevel characterization can be stated. `prChar-fwd` takes three hypotheses and concludes the path `Q ≡ pr U W`. The first two are truncated existential statements: merely some member `w` of `Q` carries `SglOf U`, and merely some member `w` of `Q` carries `PairOf U W`. The third is the universal clause: every member `y` of `Q` merely is a singleton of `U` or a pair of `U` and `W`. Note that the outer set of `pr U W` is an unordered pair whose two members encode the ordered components; `Q` will be shown equal to that outer pair via `pair-char`. ```agda sglOf-subst {U} e = subst (SglOf U) (sym e) (sglOf⁅⁆ U) pairOf-subst : {U W w : V ℓ} → w ≡ ⁅ U , W ⁆ → PairOf U W w pairOf-subst {U} {W} e = subst (PairOf U W) (sym e) (pairOf⁅⁆ U W) prChar-fwd : (Q U W : V ℓ) → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁ ``` The first two hypotheses each provide, merely, a member of `Q` together with a package proving that member equal to the corresponding construction. The truncation is eliminated into the membership proposition `⟨ ⁅ U ⁆s ∈ Q ⟩` or `⟨ ⁅ U , W ⁆ ∈ Q ⟩`, both of which are proposition-valued, so no choice of witness needs to be made uniform. Inside each branch, the package is converted to the path `w ≡ ⁅ U ⁆s` or `w ≡ ⁅ U , W ⁆` and the membership of `w` is transported along it, yielding membership of the construction in `Q`. These are exactly the first two arguments `pair-char` requires with `⁅ U ⁆s` and `⁅ U , W ⁆` in place of `u` and `v`. ```agda → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁ → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁) → Q ≡ pr U W prChar-fwd Q U W h₁ h₂ h₃ = pair-char Q ⁅ U ⁆s ⁅ U , W ⁆ (PT.rec ((⁅ U ⁆s ∈ Q) .snd) ``` The universal clause needs no elimination at all: for each member `y` of `Q`, the truncated disjunction of packages is mapped through the conversions `sglOf→≡` and `pairOf→≡`, producing the truncated statement that `y` merely equals `⁅ U ⁆s` or `⁅ U , W ⁆`. That is the third argument of `pair-char`. Its conclusion is then `Q ≡ ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`, which is by definition `Q ≡ pr U W`. The converse `prChar-bwd` is a matter of exhibiting the three hypotheses for the Kuratowski pair itself. ```agda (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (sglOf→≡ h) hw }) h₁) (PT.rec ((⁅ U , W ⁆ ∈ Q) .snd) (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (pairOf→≡ h) hw }) h₂) (λ y hy → PT.map (Sum.map sglOf→≡ pairOf→≡) (h₃ y hy)) prChar-bwd : (Q U W : V ℓ) → Q ≡ pr U W ``` Given a path `Q ≡ pr U W`, the three hypotheses are produced in order. The helper `inQ` moves a membership in `pr U W` to a membership in `Q` by transporting along the reversal of the path, and it will feed all three components. ```agda → (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁) × ((∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁) × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁)) prChar-bwd Q U W e = h₁ , h₂ , h₃ where ``` The first existential is witnessed by `⁅ U ⁆s` itself: it belongs to `pr U W` because the outer pair contains its first component, an instance of `∈pair-introL` at the reflexive path, and after transport through `inQ` this membership holds in `Q`; it carries `SglOf U` by the package `sglOf⁅⁆`. The second is the same with `⁅ U , W ⁆`, `∈pair-introR`, and `pairOf⁅⁆`. Both are sealed with the truncation, as their types demand; the chosen witnesses are enough because the target is merely an existence statement. ```agda inQ : {z : V ℓ} → ⟨ z ∈ pr U W ⟩ → ⟨ z ∈ Q ⟩ inQ {z} h = subst (λ w → ⟨ z ∈ w ⟩) (sym e) h h₁ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁ h₁ = ∣ ⁅ U ⁆s , (inQ (∈pair-introL refl) , sglOf⁅⁆ U) ∣₁ h₂ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁ ``` The universal clause reduces to the classification of the pair construction. For a member `y` of `Q`, transport along the path gives membership of `y` in `pr U W`, and `∈pair-elim` converts that into the truncated disjunction `y ≡ ⁅ U ⁆s` or `y ≡ ⁅ U , W ⁆`. Each side is upgraded to the corresponding package by the transport lemmas `sglOf-subst` and `pairOf-subst`, so the map sends the disjunction of paths to the disjunction of packages, without ever unfolding either construction. ```agda h₂ = ∣ ⁅ U , W ⁆ , (inQ (∈pair-introR refl) , pairOf⁅⁆ U W) ∣₁ h₃ : (y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁ h₃ y y∈Q = PT.map (Sum.rec (λ q → inl (sglOf-subst q)) (λ q → inr (pairOf-subst q))) (∈pair-elim (subst (λ w → ⟨ y ∈ w ⟩) e y∈Q)) ``` ## The readers The external characterizations now become object-language formulas. Each reader takes the de Bruijn positions it speaks about as arguments, so the same definition serves at any depth of nesting. The bookkeeping is the standard one for bounded quantification: a bounded quantifier binds a fresh variable at position zero and pushes the existing positions one step outward, so a position mentioned under one binder appears as its successor. Because every clause is an atom, a conjunction or disjunction, or a quantifier bounded by a variable of the environment, every reader is Δ₀ and its bounding sets are visible directly in its shape. The singleton reader `sglAt k i` says of the sets assigned to positions `k` and `i` that the one at `i` is the singleton of the one at `k`. Its first conjunct is the atom `var i ∈̇ var k`; the second bounds a quantifier over the members of `var k` and, inside it, compares the freshly bound variable at position zero with `var (suc i)`, which is the position `i` after the one-step shift under the binder. A set satisfies this reading exactly when it has a member equal to `k`'s value and no other members, the content of `SglOf`. ```agda sglAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n sglAt k i = (var i ∈̇ var k) ∧̇ (∀̇∈ (var k) (var zero ≐ var (suc i))) ``` The unordered-pair reader `pairAt k i j` adds the second component and weakens the universal clause to a disjunction. Under the bounded quantifier, the fresh variable at position zero is compared with both `var (suc i)` and `var (suc j)`, the two shifted argument positions. Read externally, a set satisfies it when the values at `i` and `j` both belong to it and every member merely equals one of the two, which is exactly the package `PairOf`. Note the fixity of `_∧̇_` and `_∨̇_` governs only how these expressions parse; no associativity of the connectives is being asserted. ```agda pairAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n pairAt k i j = (var i ∈̇ var k) ∧̇ ((var j ∈̇ var k) ∧̇ (∀̇∈ (var k) ((var zero ≐ var (suc i)) ∨̇ (var zero ≐ var (suc j))))) ``` The assembled pair reader puts the two smaller readers together with the three clauses of the metalevel characterization: some member is the singleton, some member is the pair, and every member is one of the two. Each bounded quantifier is over the members of the value at `q`, and the two argument positions are shifted by one beneath each binder, so the inner readers again address the fresh variable as position zero. The first clause bounds an existential over the members of `var q` with body `sglAt zero (suc u)`: the fresh variable at position zero is the candidate member, and `suc u` is the position of `u` after the shift. The second clause is the same with `pairAt`, now mentioning the shifted positions of both `u` and `v`. The third bounds a universal quantifier whose body is the disjunction of the two readers: every member of the value at `q` is merely a singleton or a pair. The existential witnesses and the either-or classification remain propositionally truncated, exactly as in `SglOf` and `PairOf`; the object language does not select a member, it only says that one merely exists. ```agda prAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n prAt q u v = (∃̇∈ (var q) (sglAt zero (suc u))) ∧̇ ((∃̇∈ (var q) (pairAt zero (suc u) (suc v))) ∧̇ (∀̇∈ (var q) (sglAt zero (suc u) ∨̇ pairAt zero (suc u) (suc v)))) Δ₀-prAt : ∀ {n} (q u v : Fin n) → Δ₀ (prAt q u v) ``` Boundedness is certified syntactically. The checker `checkΔ₀` traverses the assembled formula, and since every node is an atom, a connective, or a quantifier bounded by a variable, it accepts with the trivial certificate `tt`, yielding `Δ₀-prAt`. This places the reader in the bounded class whose satisfaction is absolute between transitive models, a fact the later chapters on absoluteness rely on. ```agda Δ₀-prAt q u v = checkΔ₀ (prAt q u v) tt ``` ## Adequacy The final theorem connects the object-language reader with its external meaning. Since satisfaction takes values in `hProp`, the statement is itself a path of truth values: the proposition `γ ⊨ prAt q u v` is identified with the proposition that the value at `q` equals the Kuratowski pair of the values at `u` and `v`, packaged with the proof that this equality type is a proposition because `V ℓ` is an h-set. Unfolding the satisfaction of the three connectives and the bounded quantifiers turns the left side into exactly the three hypotheses that `prChar-fwd` and `prChar-bwd` consume, so the adequacy proof composes two existing arguments rather than proving anything new. Both sides of the displayed path are truth values. On the right, the equality type `⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)` is paired with `setIsSet _ _`, the witness that equality of two h-set elements is a proposition; this pairing is exactly how an `hProp` is built. The proof then supplies the two directions of the underlying iff, and `⇔toPath` promotes them to the path of propositions. ```agda prAt-adequate : ∀ {n} (q u v : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ prAt q u v) ≡ ((⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)) , setIsSet _ _) prAt-adequate q u v γ = ⇔toPath (λ { (h₁ , h₂ , h₃) → prChar-fwd _ _ _ h₁ h₂ h₃ }) ``` The forward direction receives the satisfaction of `prAt q u v`, which by the semantics of `_∧̇_` and the bounded `∃̇∈` and `∀̇∈` is a triple: the truncated existence of a member satisfying the singleton reader, the truncated existence of one satisfying the pair reader, and the universal clause. These are precisely the three arguments of `prChar-fwd`, and they return the path to `pr U W`. The backward direction takes the equality path and hands it to `prChar-bwd`, which packages it into the three clauses that the semantics reassembles into satisfaction. Nothing in either direction inspects how any set was constructed. ```agda (λ e → prChar-bwd _ _ _ e) ``` ## Recap `prAt` reads a Kuratowski pair from inside the object language; it is Δ₀ and adequate, its satisfaction being a path to equality with `pr` of the assigned values. Everything a certificate needs in order to destructure a code is now available in bounded form, with no recursion and no comparison of code values. The chapters that follow build certificates on top of these readers.