---
title: "The least-witness map inside a constructible stage"
module: L.GCH.LeastWitnessMap
lang: en
site: "Bedrock"
description: "Least witnesses form a definable map"
stage: "Proving GCH"
reading_order: 112
canonical: https://bedrock.institute/en/L.GCH.LeastWitnessMap.html
html: L.GCH.LeastWitnessMap.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/LeastWitnessMap.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Basic, L.Choice.StageOrders, L.Choice.InternalWellOrder, L.WellOrder.Base, L.DefinableInjection, L.GCH.CardinalSquareLaw, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.LeastWitnessMap.md, https://bedrock.institute/ja/L.GCH.LeastWitnessMap.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The least-witness map inside a constructible stage

Suppose that, for each input `x ∈ X`, we know only under propositional truncation that some `w ∈ Lset γ` satisfies `P(w,x)`. Such pointwise existence does not yet give a graph inside `L`, because one formula must determine a unique value. This chapter uses the canonical strict well order of the fixed stage to choose its least satisfying candidate, expresses that choice by a formula, and collects the graph as a set of `L`. The minimum is relative to this stage and this order, and `P` itself may have many witnesses.

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

Classical logic enters through the fixed excluded-middle hypothesis, which already underlies the canonical stage order. At the actual least-element search, it has a precise role: during well-founded descent it decides whether a smaller satisfying stage member merely exists. Propositional truncation is eliminated only into the total type of least witnesses, after that type has been proved to be a proposition; this gives no general way to extract arbitrary witnesses.

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

Fix a universe level `ℓ` and excluded middle for propositions at level `ℓ-suc ℓ`. Every selected witness and every graph constructed below is relative to this single hypothesis and to the fixed stage order introduced later.

```agda
module L.GCH.LeastWitnessMap {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The desired graph must be expressed in the first-order language of sets. Besides saying that `P(w,x)` holds, its formula must say that `w` lies in the chosen stage and that no smaller member of that stage also satisfies `P`. A bounded universal quantifier expresses the latter condition, while renaming lets the original two-variable formula keep its meaning after the smaller candidate is inserted into the environment.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∀̇∈ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

Two views of the stage order are needed. The host-level strict well order supports least-element search, while a constructible set `Rγ` of coded ordered pairs lets the same comparison appear inside the object-language graph formula. The representation lemmas pass between these views; they do not identify them by definition.

```agda
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset→isL )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf ) renaming ( Mem to MemOf )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )
```

The strict well order supplies both a least-element operation and trichotomy. The former selects a value from a merely inhabited family of candidates; the latter proves that any two candidates satisfying the complete leastness specification coincide. Once that specification is expressed by a formula, replacement collects the resulting input-value pairs into a set of `L`.

```agda
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( SWO; leastOf; lt; eq; gt ) renaming ( Tri to Tri∙ )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Graph )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
```

Propositional truncation deliberately hides which initial candidate exists. The proof may eliminate that truncation only after changing the target to the total type of least elements and proving that this target is itself a proposition. Equality of constructible sets likewise ignores their proof components, so equality of the underlying sets is enough throughout the argument.

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
```

The carrier `S` packages an ambient set together with a proof that it is constructible. Inputs and candidates can therefore occupy entries of a satisfaction environment, while the packaged stage `Lγ` and order relation `Rγ` can occur as constants in formulas. First projection returns the underlying sets needed for membership and ordered-pair coding.

```agda
open hPropStructure 𝒮ʟ using ( S )
```

Satisfaction is read in the constructible structure `𝒮ʟ`. In particular, `P` is already an object-language formula; the chapter selects witnesses for this definable relation and does not claim to turn an arbitrary host-level predicate into a definable one.

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

The original formula is evaluated in the two-entry environment `(w,x)`. When leastness introduces a bounded competitor, the environment becomes `(w',w,x)`, so the occurrence of the input must move while the new candidate `w'` occupies the first slot. Compatibility of satisfaction with renaming will justify that shift.

```agda
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
```

The indices `i0` and `i1` name the first two available de Bruijn slots. Their mathematical roles depend on the environment: in `(w,x)` they refer to the proposed value and the input, while inside the bounded environment `(w',w,x)` they refer to the competitor and the proposed value.

```agda
private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0
```

Two constructible sets with equal underlying sets are equal, by the propositionhood of constructibility; every later identification of constructible sets goes through this lift.

```agda
  S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
  S≡ = Σ≡Prop (λ v → snd (isL v))
```

## Selecting the least satisfying member

The least-witness module receives four pieces of data. The ordinal index `γ` with its ordinalness determines the stage; the set `X` constrains the inputs; the binary formula `P` is the predicate; and for every input in `X` the hypothesis asserts, merely, that some candidate from the stage satisfies the predicate there. The candidates are drawn from the whole stage `Lset γ`, while the inputs are constrained to `X`.

```agda
module Least (γ : V ℓ) (oγ : IsOrd γ) (X : S) (P : Formula S 2)
  (have : (x : S) → ⟨ fst x ∈ fst X ⟩
        → ∥ Σ[ w ∈ S ] (⟨ fst w ∈ Lset γ ⟩ × ⟨ (w ∷ x ∷ []) ⊨ P ⟩) ∥₁) where
```

The ambient stage `Lset γ` is packaged as an element `Lγ` of the constructible carrier. This package can occur as a constant in the graph formula, so the formula can bound its search to exactly the fixed candidate stage.

```agda
  opaque
    Lγ : S
    Lγ = LsetS γ oγ
```

The equation `Lγ-fst` exposes the underlying set of this opaque package as `Lset γ`. Later membership proofs cross this equation when moving between the host-level stage and the constant used by the formula.

```agda
    Lγ-fst : fst Lγ ≡ Lset γ
    Lγ-fst = refl
```

The internal relation encoder also needs the ordinal index itself as an element of the constructible universe. Every ordinal is constructible, and `oγ` supplies the ordinalness needed to obtain that fact for `γ`.

```agda
    hγ : ⟨ isL γ ⟩
    hγ = isL-ord γ oγ
```

The internal implementation of the stage order is a constructible set of coded pairs, the relation in which leastness will be expressed.

```agda
  Rγ : S
  Rγ = relL γ hγ oγ
```

The predicate `Mem x` records the restriction on inputs: it is evidence that `x ∈ X`. It imposes no condition on witness candidates, whose separate carrier is the set of members of `Lset γ` introduced next.

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst X ⟩
```

The order `orderAt γ oγ` acts on stage members rather than on arbitrary elements of `S`. The subtype `Mγ` builds the bound `c ∈ Lset γ` into every object being compared, so least-element search cannot range outside the fixed candidate stage.

```agda
  private
    Mγ : Type (ℓ-suc ℓ)
    Mγ = MemOf (Lset γ)
```

An element of `Mγ` contains an underlying set together with its membership in `Lset γ`. Every member of a constructible stage is constructible, so `memS` can promote that underlying set to the carrier `S`; the original membership proof remains available as the stage bound on the candidate.

```agda
    memS : Mγ → S
    memS c = fst c , Lset→isL γ oγ (fst c) (snd c)
```

The predicate at a candidate and an input is the object-language satisfaction of `P` in the environment placing the candidate first and the input second.

```agda
    At : S → S → hProp (ℓ-suc ℓ)
    At w x = (w ∷ x ∷ []) ⊨ P
```

The predicate `Good x` transfers the original relation to the carrier ordered by `orderAt γ oγ`: a stage member is good exactly when its associated element of `S` satisfies `P` with input `x`. Consequently the forthcoming search orders candidates from `Lset γ`; it does not order the inputs in `X` or restrict candidates to `X`.

```agda
    Good : S → Mγ → hProp (ℓ-suc ℓ)
    Good x c = At (memS c) x
```

The same underlying set may arrive with two proofs that it is constructible. Since constructibility is a proposition, `S≡` identifies the two packaged elements of `S`; transporting satisfaction along that path shows that the repackaged stage member satisfies the same instance of `P` as the original witness.

```agda
    toMem : (x w : S) (hw : ⟨ fst w ∈ Lset γ ⟩) → ⟨ At w x ⟩ → ⟨ Good x (fst w , hw) ⟩
    toMem x w hw = subst (λ v → ⟨ At v x ⟩) (S≡ refl)
```

Selection is performed after fixing an input `x` and evidence `m : x ∈ X`. The evidence authorizes the use of the pointwise existence hypothesis `have`; it neither puts the candidate in `X` nor equips `X` with an order.

```agda
  module Sel (x : S) (m : Mem x) where
```

For the fixed input, the hypothesis is mapped into the type of good stage members. This changes only the representation of each possible witness: the resulting nonemptiness remains propositionally truncated, so no particular starting member has yet been chosen.

```agda
    private
      nonempty : ∥ Σ[ c ∈ Mγ ] ⟨ Good x c ⟩ ∥₁
      nonempty = PT.map (λ { (w , hw , hp) → (fst w , hw) , toMem x w hw hp }) (have x m)
```

Now `leastOf` descends through `orderAt γ oγ` and returns an actual least good member. This is the exceptional elimination step: excluded middle decides whether descent can continue, and propositional truncation may be eliminated because the total type of a least element together with its leastness proof has already been shown to be a proposition. Neither fact alone would justify extracting an arbitrary witness from `nonempty`.

```agda
    opaque
      c : Mγ
      c = fst (leastOf (orderAt γ oγ) lem (Good x) nonempty)
```

The result of the search retains the proof that the selected member is good. Thus the passage from mere existence to an actual least element does not lose the original predicate.

```agda
      c-good : ⟨ Good x c ⟩
      c-good = fst (snd (leastOf (orderAt γ oγ) lem (Good x) nonempty))
```

Its companion clause gives the exact relative leastness needed later: any other good member of this same stage is forbidden from lying strictly below the selected one in `orderAt γ oγ`.

```agda
      minimal : (c' : Mγ) → ⟨ Good x c' ⟩ → relOf (orderAt γ oγ) c' c → Empty.⊥
      minimal = snd (snd (leastOf (orderAt γ oγ) lem (Good x) nonempty))
```

The order compares objects in `Mγ`, whereas satisfaction environments contain objects of `S`. Repackaging the chosen member as `e` crosses this interface without changing its underlying set.

```agda
    e : S
    e = memS c
```

Because goodness was defined through this same repackaging, the selected element of `S` immediately satisfies `P(e,x)`; no second choice or new search is involved.

```agda
    e-holds : ⟨ (e ∷ x ∷ []) ⊨ P ⟩
    e-holds = c-good
```

The membership component carried by the selected stage member also proves `e ∈ Lset γ`. Predicate satisfaction and the stage bound are therefore obtained from the same least candidate.

```agda
    e∈Lγ : ⟨ fst e ∈ Lset γ ⟩
    e∈Lγ = snd c
```

For an input `x` equipped with `m : x ∈ X`, the function `fn` returns this selected candidate. Its domain evidence is explicit because the existence hypothesis is available only on `X`.

```agda
  fn : (x : S) → Mem x → S
  fn x m = Sel.e x m
```

At every such domain input, the chosen value satisfies the original formula in the environment `(fn(x),x)`.

```agda
  fn-holds : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ P ⟩
  fn-holds x m = Sel.e-holds x m
```

The same value lies in `Lset γ`. This separate range statement will later place the definable map in codomain `Lγ`; it does not say that the value lies in the input set `X`.

```agda
  fn-in : (x : S) (m : Mem x) → ⟨ fst (fn x m) ∈ Lset γ ⟩
  fn-in x m = Sel.e∈Lγ x m
```

To state leastness in terms that can also be expressed inside `L`, assume that a competitor `w'` is recorded below `fn(x)` by the internal relation `Rγ`. The reading lemma `relL-rep` converts this coded entry into the host-level comparison used by `orderAt γ oγ`, where the minimality of the selected member refutes it. The conclusion excludes only satisfying competitors in `Lset γ` and only with respect to this fixed order.

```agda
  fn-least : (x : S) (m : Mem x) (w' : S) → ⟨ fst w' ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
           → ⟨ pr (fst w') (fst (fn x m)) ∈ fst Rγ ⟩ → Empty.⊥
  fn-least x m w' hw' hp hr = Sel.minimal x m (fst w' , hw') (toMem x w' hw' hp)
    (relL-rep γ hγ oγ (fst w' , hw') (Sel.c x m) hr)
```

The host-level specification `TWit w x` combines the three facts that the graph formula must express: `P(w,x)`, membership of `w` in the fixed stage, and the absence of a stage member satisfying `P` strictly below `w` in `orderAt γ oγ`. This is a specification of a graph value, before the graph is collected as an internal table.

```agda
  TWit : (w x : S) → Type (ℓ-suc ℓ)
  TWit w x =
      ⟨ (w ∷ x ∷ []) ⊨ P ⟩
    × ⟨ fst w ∈ Lset γ ⟩
    × ((w' : S) → ⟨ fst w' ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
```

The last component tests any `w'` that lies in `Lset γ` and satisfies `P(w',x)`. If the coded pair `(w',w)` belonged to `Rγ`, it would say that `w'` is strictly smaller in the fixed stage order, and the specification refutes precisely that possibility.

```agda
        → ⟨ pr (fst w') (fst w) ∈ fst Rγ ⟩ → Empty.⊥)
```

Uniqueness is proved only among candidates satisfying the complete `TWit` specification. The original predicate `P` may have many witnesses in the stage; what cannot happen in a strict total order is that two distinct candidates both satisfy `P` and both have no smaller satisfying candidate. Trichotomy reduces the comparison with the selected value to the three cases handled next.

```agda
  fn-unique : (x : S) (m : Mem x) (w : S) → TWit w x → fst w ≡ fst (fn x m)
  fn-unique x m w (hp , hw , mn) = go (SWO.tri∙ (orderAt γ oγ) c' (Sel.c x m))
    where
    c' : Mγ
    c' = fst w , hw
```

If the alternative candidate were strictly below the selected one, leastness would be contradicted; if the two stage members coincided, their underlying sets would be equal.

```agda
    go : Tri∙ (relOf (orderAt γ oγ) c' (Sel.c x m)) (c' ≡ Sel.c x m)
              (relOf (orderAt γ oγ) (Sel.c x m) c')
       → fst w ≡ fst (fn x m)
    go (lt k) = Empty.rec (Sel.minimal x m c' (toMem x w hw hp) k)
    go (eq q) = cong fst q
```

If the selected candidate were strictly below the alternative, the alternative's own leastness would be contradicted, with the missing comparison supplied by the filling direction of the internal relation.

```agda
    go (gt k) = Empty.rec (mn (fn x m) (fn-in x m) (fn-holds x m)
      (relL-fill γ hγ oγ (Sel.c x m) c' k))
```

Under the bounded quantifier the environment is `(w',w,x)`, whereas `P` expects `(candidate,input)`. The renaming therefore sends its variable 0 to slot 0, still `w'`, and its variable 1 to slot 2, now `x`; slot 1 is reserved for the proposed value `w` against which `w'` is compared.

```agda
  private
    ρ : Fin 2 → Fin 3
    ρ zero       = zero
    ρ (suc zero) = suc (suc zero)
```

Agreement records exactly those two identifications: reading variable 0 from `(w',w,x)` gives the first entry of `(w',x)`, and reading variable 1 after renaming gives the second. This pointwise agreement is the premise needed to transport satisfaction of the whole formula `P`.

```agda
    ag : (w' w x : S) → Ren.Agrees ρ (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ [])
    ag w' w x zero       = refl
    ag w' w x (suc zero) = refl
```

The leastness formula ranges over `w' ∈ Lγ` and denies the conjunction of two claims: the coded pair `(w',w)` belongs to `Rγ`, and `P(w',x)` holds. Semantically it says that no candidate in the fixed stage lies below `w` in `orderAt γ oγ` while also witnessing the original predicate for the same input.

```agda
  opaque
    private
      leastFo : Formula S 2
      leastFo = ∀̇∈ (con Lγ) (¬̇ (appC Rγ i0 i1 ∧̇ renameFo ρ P))
```

Compatibility with renaming now identifies the two readings of `P`: evaluating `renameFo ρ P` in `(w',w,x)` is the same as evaluating `P` directly in `(w',x)`. The current proposed value `w` is deliberately absent from the predicate test on the competitor; it occurs only in the order comparison `(w',w)`.

```agda
      ren : (w' w x : S)
          → ⟨ (w' ∷ w ∷ x ∷ []) ⊨ renameFo ρ P ⟩ ≡ ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
      ren w' w x = cong ⟨_⟩ (Ren.⊨-rename ρ P (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ []) (ag w' w x))
```

The full graph formula conjoins the original predicate with stage membership and the leastness clause: a value is recorded exactly when it satisfies the predicate, lies in the fixed stage, and is least among stage members that do.

```agda
    fo : Formula S 2
    fo = P ∧̇ ((var i0 ∈̇ con Lγ) ∧̇ leastFo)
```

Reading `fo` outward recovers the three parts of the semantic specification: `P(w,x)`, membership `w ∈ Lset γ`, and the absence of a satisfying member of that stage recorded below `w` by the internal order. The formula `fo` itself does not contain the condition `x ∈ X`; that restriction is imposed when `fo` is used as the graph formula of `Dmap`. Thus `X` controls the inputs on which a value must be defined, while `Lset γ` controls the candidates compared for that input.

```agda
    fo-out : (w x : S) → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩ → TWit w x
    fo-out w x (hp , (hl , hm)) =
        hp
      , subst (λ v → ⟨ fst w ∈ v ⟩) Lγ-fst hl
      , λ w' hw' hp' hr → lower (hm w' (subst (λ v → ⟨ fst w' ∈ v ⟩) (sym Lγ-fst) hw')
```

To obtain the minimality component of `TWit`, fix a competitor `w'` and assume the semantic facts that `pr(w',w) ∈ Rγ` and `P(w',x)`. The proof uses `appC-adequate` and renaming in the inward direction to turn these facts into satisfaction of the two conjuncts negated by `fo`; the bounded clause then yields the contradiction. The relation entry is an object-language encoding of the stage-order comparison, not a definitional equality with `relOf (orderAt γ oγ)`.

```agda
          ( subst ⟨_⟩ (sym (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ []))) hr
          , transport (sym (ren w' w x)) hp' ))
```

Conversely, a witness satisfying `TWit` determines a proof of the graph formula. Its first two components establish `P(w,x)` and `w ∈ Lset γ`. For the bounded minimality clause, take any `w'` in that same level and suppose that the encoded order places `w'` before `w` and that `P(w',x)` holds; the last component of `TWit` rules out exactly this conjunction.

```agda
    fo-in : (w x : S) → TWit w x → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩
    fo-in w x (hp , hl , mn) =
        hp
      , subst (λ v → ⟨ fst w ∈ v ⟩) (sym Lγ-fst) hl
      , λ w' hw' hc → lift (mn w' (subst (λ v → ⟨ fst w' ∈ v ⟩) Lγ-fst hw')
```

Renaming and application adequacy put those two assumptions into the forms expected by semantic minimality. Together, `fo-out` and `fo-in` show that `fo` expresses exactly the fixed-level least-witness specification. They add neither uniqueness of witnesses for the original predicate nor any comparison with candidates outside `Lset γ`.

```agda
          (transport (ren w' w x) (snd hc))
          (subst ⟨_⟩ (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ [])) (fst hc)))
```

This exact correspondence makes the selection definable. The map has input set `X` and codomain `Lγ`: for each proof that `x ∈ X`, its value is `fn x m`, and the earlier level-membership theorem places that value in `Lγ`. The graph formula is read in the environment `(value,input)`, so its first variable denotes the selected witness and its second variable denotes the input.

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = X ; cod = Lγ ; fn = fn
    ; into = λ x m → subst (λ v → ⟨ fst (fn x m) ∈ v ⟩) (sym Lγ-fst) (fn-in x m)
    ; graph = fo
```

At the selected value, the three facts already proved supply a proof of `fo`: the value satisfies `P`, lies in the candidate level, and has no smaller satisfying competitor there. Conversely, any value satisfying `fo` carries this full least-witness specification and is therefore equal to the selected value. This uniqueness comes from the two candidates' leastness and trichotomy of `orderAt γ oγ`, not from uniqueness of `P`-witnesses; equality of their underlying sets lifts to equality in `S` because constructibility evidence is propositional.

```agda
    ; defines = λ x m → fo-in (fn x m) x (fn-holds x m , fn-in x m , fn-least x m)
    ; only = λ x m w h → S≡ (fn-unique x m w (fo-out w x h)) }
```

Once a formula defines one value for every input in `X`, replacement can collect those values inside `L`. Applied to `Dmap`, the graph construction provides a constructible set of ordered pairs together with the two directions needed to use its membership relation.

```agda
  private
    module Gr = Graph Dmap using ( F; F-in; pair-out )
```

Call this collected set `T`. Its entries are ordered pairs `(x,fn(x))`, with the input first and the selected value second. This reverses the order used by formula satisfaction, whose environment was `(value,input)`; keeping the two conventions distinct prevents the graph formula from being mistaken for the internal table itself.

```agda
  T : S
  T = Gr.F
```

For every `x ∈ X`, the table contains the pair `(x,fn(x))`. Hence later arguments may refer to the choices through membership in one constructible set, rather than making a separate choice from the merely inhabited family for each input.

```agda
  T-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst T ⟩
  T-in = Gr.F-in
```

Conversely, an entry `(x,w) ∈ T` yields evidence `x ∈ X` and equality of the underlying set of `w` with that of the selected value `fn(x)`. Table membership does not return the leastness proof itself. In `HullCounting`, this table is used to synchronize choices that were previously available only under propositional truncation. When an injection is needed, a separate reverse-functionality hypothesis for the underlying relation proves that a fixed related candidate cannot correspond to two different inputs; injectivity is not a consequence of least selection alone.

```agda
  T-out : (x w : S) → ⟨ pr (fst x) (fst w) ∈ fst T ⟩
        → Σ[ m ∈ Mem x ] (fst w ≡ fst (fn x m))
  T-out = Gr.pair-out
```