Bedrock可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。
交互式目录 · 依赖图固定宇宙层级 ℓ 与这一排中律实例。这里的数学问题，是怎样从宿主层的取值规则得到一个可由 L 量化的集合。取值规则本身不会被放入 L；一条公式在 L 的某个集合上描述它的值，替换据此形成可构造的函数图，再由单射性证明为该图配上内部基数比较所需的编码。
module L.DefinableInjection {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
在 L 外部描述一条取值规则，并不等于已经有了一个可供 L 量化的对象。要在模型内部比较基数，需要一个由有序对组成的可构造集合来记录这些取值。因此，本章的中心问题是：可定义性与逐点唯一性怎样使替换定理能够收集这张函数图。
唯一的经典参数是层级 ℓ-suc ℓ 上的排中律。本章中的初等步骤，例如证明唯一性、运输成员关系，以及把命题截断消去到命题中，都是构造性的。这个参数在一般替换定理把函数图收集成 L 的元素时起作用；全程不使用任何形式的选择公理。
这里须区分三类对象。公式属于一阶语言，其常元是可构造论域的元素；满足关系在 L 上的结构中解释该公式；pr 则是在外围层级中编码底层集合有序对的柯拉托夫斯基对。稍后读取定义公式时，值在前、输入在后；收集所得函数图的条目则是 pr(输入,值)。
证明依次经过三种数学形式。递归由定义域、取值公式，以及定义域每一点的满足值纤维可缩这一证明组成。函数图构造用替换收集有序对，并证明单值性与恰当定义域。最后，injAt 表达尚缺的单射条件：两个条目若有相同输出，其输入便相等。
对集合 a 与 b，InjCode F a b 恰有四个分量：函数图 F 是单值的，其定义域恰为 a，它满足单射性，并且其中出现的每个值都属于 b。四个条件都有对应的对象语言公式，其中取值范围条件使用此前构造的 valuesInAt 公式。InjL a b 则把这样的 F 及其编码之存在作命题截断。
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 _⊨_ )
把单射码读作一条公式
InjCode 的四个条款可以由一条带三个指定槽位的对象语言公式呈现：函数图、定义域和陪域。前三个合取支复用单值性、精确定义域与单射性的公式；最后一支量化实参和取值，并断言函数图一旦联系二者，取值就属于陪域槽。因此，宿主层的值域字段并未被假定为不可见，而是在此接口处与一条经过检查的公式绑定。
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
module InjCodeAt {n : ℕ} (f A B : Fin n) (γ : Vec S n) where
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
对函数图槽作存在量化便得到 InjL 的公式，余下两个槽分别指名定义域与陪域。其语义存在量词本来就带命题截断，恰与 InjL 相同。把上面的 read 与 fill 函数映入该截断，就得到两个方向而无需选出函数图。
injLAt : ∀ {n} → Fin n → Fin n → Formula S n
injLAt A B = ∃̇ (injCodeAt zero (suc A) (suc B))
内部基数性断言：候选者的任何元素都不能接受一条从候选者出发的单射。下式准确表达这一点：约束一个可能的较小元素后，「它属于候选者」蕴含 injLAt 公式的否定。其读取只需转换单射公式；外围的全称量词、蕴涵与否定会直接计算成 IsCardinalL 已使用的函数类型。
cardinalAt : ∀ {n} → Fin n → Formula S n
cardinalAt K = ∀̇ ((var zero ∈̇ var (suc K))
⇒̇ ¬̇ injLAt (suc K) zero)
两项类型论事实控制着这段证明。若依值对的第二分量取值于命题，Σ≡Prop 就能把第一分量之间的路径提升为整对之间的路径。命题截断只保留是否有元素。函数图的读回引理 pair-out 可以消去一个经命题截断的来源见证，因为它的目标纤维是命题；最后一步则用 ∣_∣₁ 隐去具体的函数图与编码。这两次操作都没有全局选出一族见证。
论域 S 来自 L 上的结构：元素 x : S 由外围集合 x .fst 与它可构造的命题性证书组成。元素记号取自外围层级，所以记录中的表达式明确比较底层集合，例如 x .fst ∈ˢ dom .fst。当构造必须返回 L 的元素时，可构造性证书仍保留在第二分量中。
记号 _⊨_ 表示外围层级限制到可构造集合所得结构中的满足关系。因此，(y ∷ x ∷ []) ⊨ graph 用 L 的元素填入 graph 的两个自由槽位来解释它。名称 AbsL 并不声称任意公式在 L 与外围层级之间绝对；本章使用的是限制结构的语义与已经证明的替换定理。
函数可定义的含义
一项 DefinableMap 首先指定 L 的两个元素 dom 与 cod，并不假设它们是序数或基数。宿主层取值规则 fn 只对一对数据有定义：x : S 以及 x 属于 dom 的证据 m；定义域之外无需给出值。类型允许 fn x m 提及 m。由于成员关系是命题，任意两份此类证明都相等，再由合同性可知相应取值相等。字段 into 证明每个选定值都属于 cod。
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 ⟩
其余字段把宿主层取值与对象语言公式联系起来。graph 有两个自由槽位，可以含有来自 S 的常元，并不要求是 Δ₀ 公式。对每个 x ∈ dom，defines 证明以所选值在前、x 在后的环境满足该公式；only 则证明任何满足公式的 y 都在 S 中等于该所选值。这些条件不约束 dom 之外的输入，only 也不假设候选 y 属于 cod。所选值落入陪域由独立的字段 into 给出。
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
把图的表项编码成有序对
函数图由一个集合表示，因此每个输入输出表项都要先表示为有序对。定义公式在第一个语义槽位中读取函数值，在第二个槽位中读取输入；集合编码则把相应表项存为 pr(输入,函数值)。构造函数图并在随后读回其内容时，必须始终区分这两种次序。
在 L 内部构造函数图
第一项构造只假设可定义性与函数性。它从 M 形成一个属于 L 的完整函数图，并给出准确写入与读取有序对条目的方法。单射性留到下一阶段：同一函数图构造也适用于无需单射的可定义映射，例如最小见证表。
module Graph (M : DefinableMap) where
open DefinableMap M public
为满足递归所需的假设，保留 dom 与 graph，并证明定义域每一点的满足值纤维都有中心。该中心是 (fn x m, defines x m)，即给定取值及其满足证明。成员关系证据 m 直接传给 fn，所以这一步不会把取值规则扩张到 dom 之外。此处既不需要 into，也不需要单射性。
private
R : Recursion
R = record
{ dom = dom ; graph = graph
; funct = λ x m → (fn x m , defines x m)
还须把每个候选 (y,h) 收缩到该中心。字段 only 给出 y ≡ fn x m，而可缩性要求一条从中心到候选的路径，因此代码使用 sym。第二分量是满足证明，因而为命题；所以 Σ≡Prop 能把反向后的取值相等提升为整个依值对的相等。这样便构造性地证明了所需的唯一存在。
, λ { (y , h) → Σ≡Prop (λ w → ((w ∷ x ∷ []) ⊨ graph) .snd) (sym (only x m y h)) } }
现在由替换把有序对取值收集成可构造集合 F。辅助配对公式协调两种次序：原关系按 (值,输入) 解释，而 F 的元素是 pr(输入,值)。F-in 写入每个指定条目，F-out 则在命题截断下说明每个元素都来自这样的条目。固定 x 与 y 后，pair-out 把 pr(x,y) 属于 F 加强为一份定义域证明与等式 y = fn(x)。这次消去是合法的，因为 Fib x y 是命题，其中用到成员关系证明的证明无关性以及 V 中相等取值于命题。由这些读式可证明 sv 所表达的单值性，以及 dm 所表达的定义域恰为 dom。形成 F 的步骤使用替换定理，因而依赖给定的排中律；后续读取没有引入选择。
open RecursionGraph R public
using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )
最终编码的第四项条件是取值落入陪域。给定实际函数图条目 pr(x,fst .fst y) ∈ F .fst，pair-out 给出 m : x ∈ dom 与 e : y .fst ≡ (fn x m) .fst。字段 into x m 证明 (fn x m) .fst 属于 cod .fst。因此，成员关系必须沿 sym e 从所选值运输回 y，从而得到 y ∈ cod。这只证明像包含于陪域，并不证明陪域的每个元素都会出现。
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
从外部单射性得到编码单射
要把这张函数图变成单射编码，还须加入真正新的单射性假设。对两个各自带有 dom 成员关系证明的输入，它断言：若所选取值的底层集合相等，则输入的底层集合相等。元素实参仍然显式出现，因为 fn 的类型依值地依赖于它们。证明无关性保证不同成员关系证明之间相容，但这条假设仍按两个输入处实际给出的证据陈述。其结论的强度恰好符合 injAt 的相等条款。
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
打开 Graph M 后，已经构造出的 F 及其性质可用于单射情形。于是同时保留两种数学上有用的结论：当后续构造必须指名或组合函数图时，可以保留这个具体的 F 及其编码；也可以使用 injL，只记住某个编码单射存在。两者的区别在于具体数据与其命题性存在。
open Graph M public
公式 injAt zero 固定输出 y，比较两个输入 x 与 x'：若 pr(x,y) 和 pr(x',y) 都属于 F，则两个输入相等。对第一条目应用 pair-out 得到 e : y = fn(x)，对第二条目应用它则得到 e' : y = fn(x')，并同时得到所需的两份定义域证明。因此，sym e ∙ e' 正是路径 fn(x) = fn(x')；宿主层假设 inj 把它化为 x = x'，injAt-in 再把这一性质转成满足判断 ij。这段论证使用的是单射性，而不仅是 only；only 比较固定输入处的输出，它支持的是单值性。
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'))
四元组 sv , dm , ij , ran 依次填入 InjCode F dom cod 的四个字段。其中，sv 证明单值性，dm 证明函数图的定义域恰为 dom，ij 证明对象语言中的单射性；三者都在环境 F ∷ dom ∷ [] 中陈述。最后的 ran 在宿主层断言 F 中出现的值属于 cod。这份编码没有断言满射性，所以它描述的是到 cod 的单射，而不是双射。
code : InjCode F dom cod
code = sv , dm , ij , ran
最后，把具体的对 (F,code) 放入命题截断。所得项 injL : InjL dom cod 断言存在一张带单射编码的可构造函数图，同时忘去所构造的是哪一张图。基数比较需要的正是这个命题，并可在目标仍为命题时对它作消去。若某项构造需要具体数据，实例化后的模块中仍可分别使用 F 与 code。因此，被内化到 L 中的是编码后的函数图，而不是外部取值规则本身。
injL : InjL dom cod
injL = ∣ F , code ∣₁