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.

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

  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.

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.

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.

  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 ⟧ γ).

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.

∈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.

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

    (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₁.

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.

  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.

  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 ⁆.

  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.

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.

    ⟨ 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.

  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.

  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.

  → ∥ Σ[ 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.

    (λ { (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.

  → (∥ Σ[ 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.

  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.

  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.

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.

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.

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.

Δ₀-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.

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.

  (λ 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.