---
title: "Turning a definable injection into an internal code"
module: L.DefinableInjection
lang: en
site: "Bedrock"
description: "Turning a definable injection into an internal code"
stage: "Ordinals, injections and cardinals"
reading_order: 90
canonical: https://bedrock.institute/en/L.DefinableInjection.html
html: L.DefinableInjection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/DefinableInjection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Recursion, L.Recursion.Graph, L.Coding.Injection, L.Cardinal]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/L.DefinableInjection.md, https://bedrock.institute/ja/L.DefinableInjection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Turning a definable injection into an internal code

A rule described outside `L` is not yet an object over which `L` can quantify. To compare cardinalities internally, we need a constructible set of ordered pairs recording the rule's values. The central question is therefore how definability and pointwise uniqueness let Replacement collect that graph.

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

The sole classical parameter is excluded middle at level `ℓ-suc ℓ`. The elementary steps in this chapter, such as proving uniqueness, transporting membership, and eliminating a propositional truncation into a proposition, are constructive. The parameter matters when the general Replacement theorem collects the graph as an element of `L`; no form of choice is used.

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

Fix a universe level `ℓ` and this instance of excluded middle. The mathematical problem is to pass from a host-level rule to a set that `L` can quantify over. The rule itself is not inserted into `L`. Instead, a formula describes its values on a set of `L`, Replacement forms a constructible graph, and an injectivity proof equips that graph with the code used for internal cardinal comparisons.

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

Three kinds of object must be kept distinct. A formula belongs to the first-order language whose constants are elements of the constructible carrier; satisfaction interprets it in the structure on `L`; and `pr` is the ambient Kuratowski code for an ordered pair of underlying sets. Later the defining formula will be read with the value first and the input second, while an entry of the collected graph is `pr(input,value)`.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

The proof passes through three mathematical forms. A recursion consists of a domain, a value formula, and a proof that the satisfying-value fiber at each domain point is contractible. Its graph construction uses Replacement to collect ordered pairs and proves single-valuedness and the exact domain. Finally, `injAt` expresses the remaining injectivity condition: two entries with the same output have equal inputs.

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )
```

For sets `a` and `b`, `InjCode F a b` has exactly four components. The graph `F` is single-valued, has domain exactly `a`, is injective, and every value appearing in it belongs to `b`. The first three components are satisfaction judgments for object-language formulas; the fourth is a host-level range condition. `InjL a b` propositionally truncates the existence of such an `F` and its code.

```agda
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
```

Two type-theoretic facts govern the proof. When the second component of a dependent pair is proposition-valued, `Σ≡Prop` lifts a path between first components to a path between the pairs. A propositional truncation retains only inhabitedness. The graph reader `pair-out` may eliminate a truncated origin because its target fiber is a proposition, while the final step uses `∣_∣₁` to hide the particular graph and code. Neither operation selects a global family of witnesses.

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

The carrier `S` comes from the structure on `L`: an element `x : S` consists of an ambient set `fst x` together with a propositional certificate that it is constructible. Membership notation is taken from the ambient hierarchy, so expressions in the record explicitly compare underlying sets, such as `fst x ∈ˢ fst dom`. The certificates remain available in the second components whenever a construction must return an element of `L`.

```agda
open hPropStructure 𝒮ʟ using ( S )
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

The notation `_⊨_` is satisfaction in the structure obtained by restricting the ambient hierarchy to constructible sets. Thus `(y ∷ x ∷ []) ⊨ graph` evaluates `graph` with elements of `L` in its two free slots. The name `AbsL` does not assert that arbitrary formulas are absolute between `L` and the ambient hierarchy; this chapter uses the restricted semantics and the already proved Replacement theorem.

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

## What it means for a function to be definable

A `DefinableMap` first specifies two elements `dom` and `cod` of `L`, with no assumption that they are ordinals or cardinals. Its host-level rule `fn` is defined only for a pair consisting of `x : S` and evidence `m` that `x` belongs to `dom`; no value outside the domain is required. The type permits `fn x m` to mention `m`. Since membership is a proposition, any two such proofs are equal, and congruence identifies the corresponding values. The field `into` proves that every selected value belongs to `cod`.

```agda
record DefinableMap : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom cod : S
    fn      : (x : S) → ⟨ fst x ∈ˢ fst dom ⟩ → S
    into    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) → ⟨ fst (fn x m) ∈ˢ fst cod ⟩
```

The remaining fields connect the host-level values to an object-language formula. `graph` has two free slots and may contain constants from `S`; it need not be Δ₀. At every `x ∈ dom`, `defines` proves that the environment has the chosen value first and `x` second, while `only` proves that every satisfying `y` equals that chosen value in `S`. These conditions say nothing about inputs outside `dom`, and `only` does not assume that its candidate `y` belongs to `cod`. The separate field `into` supplies codomain containment for the selected values.

```agda
    graph   : Formula S 2
    defines : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩)
            → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
```

## Encoding graph entries as ordered pairs

The graph is represented as a set, so each input-output entry must first be expressed as an ordered pair. The defining formula reads the value in its first semantic slot and the input in its second, whereas the set encoding stores the corresponding entry as `pr(input,value)`. Keeping these two orders distinct is essential when the graph is constructed and later read back.

## Constructing the graph inside L

The first construction assumes only definability and functionality. From `M` it will form the complete graph as an element of `L` and obtain precise ways to insert and read its ordered-pair entries. Injectivity is deliberately postponed: the same graph construction also applies to definable maps, such as a table of least witnesses, whose purpose does not require them to be injective.

```agda
module Graph (M : DefinableMap) where
  open DefinableMap M public
```

To meet the recursion hypothesis, retain `dom` and `graph` and prove that the satisfying-value fiber at each domain point has a center. The center is the pair `(fn x m, defines x m)`: the given value together with its satisfaction proof. The membership evidence `m` is passed directly to `fn`, so this construction does not extend the rule beyond `dom`. Neither `into` nor injectivity is needed at this stage.

```agda
  private
    R : Recursion
    R = record
      { dom = dom ; graph = graph
      ; funct = λ x m → (fn x m , defines x m)
```

It remains to contract every candidate `(y,h)` to that center. The field `only` gives `y ≡ fn x m`, but contractibility asks for a path from the center to the candidate, hence the use of `sym`. The second component is a satisfaction proof and therefore a proposition. `Σ≡Prop` consequently lifts the reversed equality of values to equality of the whole dependent pairs. This establishes the required unique existence constructively.

```agda
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph)) (sym (only x m y h)) } }
```

Replacement now collects the ordered-pair values into a constructible set `F`. The auxiliary pairing formula reconciles the two conventions: the original relation is evaluated as `(value,input)`, while members of `F` are `pr(input,value)`. `F-in` inserts every prescribed entry, and `F-out` says under propositional truncation that every member has such an origin. For fixed `x` and `y`, `pair-out` strengthens membership of `pr(x,y)` to a domain proof and an equality `y = fn(x)`. This elimination is valid because `Fib x y` is a proposition, using proof irrelevance of membership and the fact that equality in `V` is proposition-valued. These readings prove `sv`, single-valuedness, and `dm`, that the domain is exactly `dom`. Forming `F` is the step that uses the Replacement theorem and hence the given excluded middle; the subsequent readings introduce no choice.

```agda
  open RecursionGraph R public
    using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )
```

The fourth condition for the eventual code is containment in the codomain. Given an actual graph entry `pr(fst x,fst y) ∈ fst F`, `pair-out` yields `m : x ∈ dom` and `e : fst y ≡ fst(fn x m)`. The field `into x m` proves membership of `fst(fn x m)` in `fst cod`. Transport must therefore follow `sym e`, from the chosen value back to `y`, to conclude `y ∈ cod`. This proves only that the image is contained in the codomain, not that every codomain element occurs.

```agda
  ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst cod ⟩
  ran x y h = subst (λ w → ⟨ w ∈ fst cod ⟩) (sym e) (into x m)
    where
    m = fst (pair-out x y h)
    e = snd (pair-out x y h)
```

## From external injectivity to a coded injection

To turn this graph into an injection code, add the genuinely new hypothesis of injectivity. For two inputs equipped with proofs of membership in `dom`, it says that equality of the underlying sets of their selected values implies equality of the underlying input sets. The membership arguments remain explicit because `fn` is dependently typed in them. Their proof irrelevance guarantees coherence between different proofs, but the hypothesis is stated with the exact evidence supplied at the two inputs. Its conclusion has precisely the strength required by the equality clause of `injAt`.

```agda
module Inj (M : DefinableMap)
           (inj : (x : S) (m : ⟨ fst x ∈ˢ fst (DefinableMap.dom M) ⟩)
                  (x' : S) (m' : ⟨ fst x' ∈ˢ fst (DefinableMap.dom M) ⟩)
                → fst (DefinableMap.fn M x m) ≡ fst (DefinableMap.fn M x' m')
                → fst x ≡ fst x') where
```

Opening `Graph M` makes the already constructed `F` and its proved properties available in the injective case. This keeps two mathematically useful conclusions at hand. One may retain the particular graph `F` together with its code when a later construction must name or combine graphs. One may instead use `injL`, which remembers only that some coded injection exists. The distinction is between concrete data and its propositional existence.

```agda
  open Graph M public
```

The formula `injAt zero` fixes an output `y` and compares two inputs `x` and `x'`: if both `pr(x,y)` and `pr(x',y)` lie in `F`, then the inputs are equal. Applying `pair-out` to the first entry gives `e : y = fn(x)`, and applying it to the second gives `e' : y = fn(x')`, together with the two required domain proofs. Hence `sym e ∙ e'` is the path `fn(x) = fn(x')`; the host-level hypothesis `inj` turns it into `x = x'`, and `injAt-in` translates this property into the satisfaction judgment `ij`. This argument uses injectivity, not merely `only`: `only` compares outputs at one fixed input and is what underlies single-valuedness.

```agda
  ij : ⟨ γ ⊨ injAt zero ⟩
  ij = injAt-in zero γ (λ y x x' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x' y q
    in inj x m x' m' (sym e ∙ e'))
```

The tuple `sv , dm , ij , ran` fills the four fields of `InjCode F dom cod` in order. Here `sv` proves single-valuedness, `dm` proves that the graph domain is exactly `dom`, and `ij` proves object-language injectivity, all in the environment `F ∷ dom ∷ []`. The final field `ran` states at host level that values occurring in `F` belong to `cod`. Nothing in this code asserts surjectivity, so it describes an injection into `cod`, not a bijection.

```agda
  code : InjCode F dom cod
  code = sv , dm , ij , ran
```

Finally, the concrete pair `(F,code)` is inserted into a propositional truncation. The resulting term `injL : InjL dom cod` states that a constructible graph carrying an injection code exists, while forgetting which graph was constructed. This is the proposition needed in cardinal comparisons and can be eliminated when the desired conclusion is again a proposition. The particular `F` and `code` remain separately available within the instantiated module when a construction needs them. Thus it is the coded graph, not the external rule itself, that has been internalized in `L`.

```agda
  injL : InjL dom cod
  injL = ∣ F , code ∣₁
```