---
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.Model, 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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```
# Turning a definable injection into an internal code
```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
```
```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax
using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
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.Model {ℓ}
using ( svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro
; valuesInAt; valuesInAt-in; valuesInAt-out )
open import L.Coding.Injection {ℓ} lem
using ( injAt; injAt-in; injAt-out )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL )
```
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.
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.
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)`.
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.
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 four conditions have matching object-language formulas, including the previously developed `valuesInAt` formula for the range condition. `InjL a b` propositionally truncates the existence of such an `F` and its code.
```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open hPropView 𝒮ʟ using ( S )
open hPropView 𝒮ᵥ using ( _∈ˢ_ )
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )
```
## Reading injection codes as one formula
The four clauses of `InjCode` can be presented by one object-language formula with three designated slots: the graph, its domain, and its codomain. The first three conjuncts reuse the formulas for single-valuedness, exact domain, and injectivity. The last conjunct quantifies over an input and output and says that whenever the graph relates them, the output belongs to the codomain slot. Thus the host-level range field is not assumed invisible; it is tied to a checked formula at this interface.
```agda
injCodeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
injCodeAt f A B = svAt f ∧̇ domAt f A ∧̇ injAt f
∧̇ valuesInAt f B
```
```agda
module InjCodeAt {n : ℕ} (f A B : Fin n) (γ : Vec S n) where
```
```agda
private
F D C : S
F = lookup f γ
D = lookup A γ
C = lookup B γ
read : ⟨ γ ⊨ injCodeAt f A B ⟩ → InjCode F D C
read (sv , dm , ij , ran) =
svAt-in zero (F ∷ D ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
, domAt-intro zero (suc zero) (F ∷ D ∷ []) (λ x →
(λ h → rec₁ ((x .fst ∈ D .fst) .snd)
(λ { (y , p) → domAt-out f A γ dm x y p }) h)
, (λ hx → domAt-in f A γ dm x hx))
, injAt-in zero (F ∷ D ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
, valuesInAt-out f B γ ran
fill : InjCode F D C → ⟨ γ ⊨ injCodeAt f A B ⟩
fill (sv , dm , ij , ran) =
svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ D ∷ []) sv x y y' p q)
, domAt-intro f A γ (λ x →
(λ h → rec₁ ((x .fst ∈ D .fst) .snd)
(λ { (y , p) → domAt-out zero (suc zero) (F ∷ D ∷ []) dm x y p }) h)
, (λ hx → domAt-in zero (suc zero) (F ∷ D ∷ []) dm x hx))
, injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ D ∷ []) ij y x x' p q)
, valuesInAt-in f B γ ran
```
Existentially binding the graph slot yields the formula for `InjL`: the remaining two slots name the domain and codomain. Its semantic existential is already propositionally truncated, exactly as `InjL` is. Mapping the preceding `read` and `fill` functions under that truncation gives both directions without choosing a graph.
```agda
injLAt : ∀ {n} → Fin n → Fin n → Formula S n
injLAt A B = ∃̇ (injCodeAt zero (suc A) (suc B))
```
```agda
module InjLAt {n : ℕ} (A B : Fin n) (γ : Vec S n) where
```
```agda
private
D C : S
D = lookup A γ
C = lookup B γ
read : ⟨ γ ⊨ injLAt A B ⟩ → InjL D C
read = map₁ (λ { (F , code) → F , InjCodeAt.read zero (suc A) (suc B) (F ∷ γ) code })
fill : InjL D C → ⟨ γ ⊨ injLAt A B ⟩
fill = map₁ (λ { (F , code) → F , InjCodeAt.fill zero (suc A) (suc B) (F ∷ γ) code })
```
Internal cardinality is the assertion that no member of a candidate receives an injection from the candidate. The formula below says exactly this: after binding a possible smaller member, membership in the candidate implies the negation of the `injLAt` formula. Its reading converts only the formula for the injection; the outer universal quantifier, implication, and negation compute to the function type already used by `IsCardinalL`.
```agda
cardinalAt : ∀ {n} → Fin n → Formula S n
cardinalAt K = ∀̇ ((var zero ∈̇ var (suc K))
⇒̇ ¬̇ injLAt (suc K) zero)
```
```agda
module CardinalAt {n : ℕ} (K : Fin n) (γ : Vec S n) where
```
```agda
private
κ : S
κ = lookup K γ
read : ⟨ γ ⊨ cardinalAt K ⟩ → IsCardinalL κ
read h δ δ∈κ inj = lower
(h δ δ∈κ (InjLAt.fill (suc K) zero (δ ∷ γ) inj))
fill : IsCardinalL κ → ⟨ γ ⊨ cardinalAt K ⟩
fill c δ δ∈κ sat = lift
(c δ δ∈κ (InjLAt.read (suc K) zero (δ ∷ γ) sat))
```
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.
The carrier `S` comes from the structure on `L`: an element `x : S` consists of an ambient set `x .fst` 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 `x .fst ∈ˢ dom .fst`. The certificates remain available in the second components whenever a construction must return an element of `L`.
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.
## 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) → ⟨ x .fst ∈ˢ dom .fst ⟩ → S
into : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩) → ⟨ (fn x m) .fst ∈ˢ cod .fst ⟩
```
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 : ⟨ x .fst ∈ˢ dom .fst ⟩)
→ ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
only : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩) (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
```
```agda
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 → ((w ∷ x ∷ []) ⊨ graph) .snd) (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(x,fst .fst y) ∈ F .fst`, `pair-out` yields `m : x ∈ dom` and `e : y .fst ≡ (fn x m) .fst`. The field `into x m` proves membership of `(fn x m) .fst` in `cod .fst`. 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 (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ y .fst ∈ cod .fst ⟩
ran x y h = subst (λ w → ⟨ w ∈ cod .fst ⟩) (sym e) (into x m)
where
m = (pair-out x y h) .fst
e = (pair-out x y h) .snd
```
## 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 : ⟨ x .fst ∈ˢ (DefinableMap.dom M) .fst ⟩)
(x' : S) (m' : ⟨ x' .fst ∈ˢ (DefinableMap.dom M) .fst ⟩)
→ (DefinableMap.fn M x m) .fst ≡ (DefinableMap.fn M x' m') .fst
→ x .fst ≡ x' .fst) 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 ∣₁
```