Bedrock编码单射
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图后续的基数论证反复在单射的两种表示之间往返：一种是公式可以量化的图，另一种是集合的小成员类型之间的实际函数。两者之间的缝隙分三层填补。对象语言首先需要一条表达图是单射的公式，它是已有单值性条款的对偶。其次，在单值性与恰当定义域的假设下，图可以读成一个真正的函数，取值仍是可构造模型的元素。最后，该函数可转移到指定定义域与值域的典范小呈现上。本章补上单射性公式，并完成 Cantor-Bernstein 与 GCH 构造所用的两层读回。
这一构造本身是构造性的。周遭论证虽带有 LEM (ℓ-suc ℓ)，下面的证明却不调用它：图的取值只以截断存在给出，但单值性使整个像原像成为命题，因此可以消去截断并取得其唯一元素，而无须选择原理。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Coding.Injection {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
设 S 为可构造模型的载体。S 的元素由 V ℓ 中的周遭集合及其可构造性证明组成，因此图的断言都针对第一投影陈述。表示图取值、单值性与恰当定义域的公式，恰好把内部满足关系与这些投影后的图事实联系起来。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _≐_; _⇒̇_; ∀̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr )
第二层读回需要典范呈现的工具：集合由索引类型与索引映射呈现，member 把索引变成显式的隶属证明，fiber 做相反的事，返回一个实际的索引而非截断的存在。Σ≡Prop 会在第二分量是命题时把依赖对的相等化归为第一分量的相等，像的原像与模型载体的对正是这样处理的。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; svAt; svAt-out; domAt; domAt-in ) open import V.Presentation {ℓ} using ( member; fiber; ↪-inj ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ ) open import Cubical.Data.Sigma using ( Σ≡Prop )
这里的真值是带着「其为命题」证明的命题，满足关系直接使用 hProp 上的逻辑联结词。满足判断 _⊨_ 是对可构造结构 𝒮ʟ 陈述的，因此像 γ ⊨ svAt zero 这样的判断经充分性等同化后谈的是投影后的集合，而非对某个周遭结构的裸满足。
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁ ) open hPropStructure 𝒮ʟ using ( S )
有界绝对性把可构造模型中的满足与赋值经 fst 投影后的满足联系起来。这座桥只在应用充分性定理时使用，并不会自行使 Extract.toFun 成为单射；单射性稍后以独立假设 ij 加入。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
对象语言中的单射性
单值性的图固定一个输入、比较输出：若两条目有相同的第一分量，其第二分量一致。单射性是它的镜像：固定一个输出、比较输入。具体地，若 (x, y) 与 (x', y) 都属于图，则 x 与 x' 的第一分量必须相等。把它写成对象语言的公式，基数论证才能在模型内部对单射图作量化。本节定义 injAt，并证明：在应用的充分性等同下，该公式成立当且仅当投影后的图具有单射性质。
公式绑定赋值 x′ ∷ x ∷ y ∷ γ：槽位 0 是 x′，槽位 1 是 x，槽位 2 是 y，原来的图槽位 f 则变为 f + 3。两个前提分别说 (x,y) 与 (x′,y) 属于该图，结论把 x 与 x′ 等同。因此它固定输出并比较输入，恰是单值性的对偶。
injAt : ∀ {n} → Fin n → Formula S n injAt f = ∀̇ (∀̇ (∀̇ ( appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)) ⇒̇ (appAt (suc (suc (suc f))) zero (suc (suc zero)) ⇒̇ (var (suc zero) ≐ var zero)))))
读回时固定变元索引 f 与模型元素组成的赋值 γ。Holds₀ x y 是投影后的事实：x 与 y 的底层集合组成的有序对属于底层图，即变元 f 在 γ 中选出的那一项。下面的两个方向都是把某条应用条款的满足判断与这个 Holds₀ 相比较，充分性路径是整个论证的枢纽。
module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where private Holds₀ : S → S → Type (ℓ-suc ℓ) Holds₀ x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ at₁ : (y x x' : S)
路径 at₁ 记录第一条应用条款在扩张赋值 x' ∷ x ∷ y ∷ γ 处的充分性：那里的满足被等同于对 (x, y) 属于图的投影事实。这一等同是命题之间的相等，由 appAt-adequate 在所给变元索引处给出，因此可以向两个方向运输。
→ ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero))) ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ)) at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero)) (x' ∷ x ∷ y ∷ γ) at₂ : (y x x' : S)
路径 at₂ 是另一条条款的同样陈述：变元 0 与 2 处的应用的满足等同于 (x', y) 属于图的投影事实。两条路径只在对码中输入哪个第一分量上不同，而这正是单射性所利用的不对称。
→ ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero))) ≡ (pr (fst x') (fst y) ∈ fst (lookup f γ)) at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero)) (x' ∷ x ∷ y ∷ γ) injAt-out : ⟨ γ ⊨ injAt f ⟩
向外的方向 injAt-out 从公式在 γ 处成立的证明与两个隶属事实 Holds₀ x y、Holds₀ x' y 出发。把三个量词实例化，得到含取式体在扩张赋值处的满足证明；再把隶属事实沿 at₁、at₂ 的反向运输，变成两条前件条款的满足证明。最后的 fst x ≡ fst x' 在模型的相等中读出。
→ (y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x' injAt-out h y x x' p q = h y x x' (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q) injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x') → ⟨ γ ⊨ injAt f ⟩
向内的方向 injAt-in 沿同样的路径正向运输：把投影的单射性质作为关于 Holds₀ 的假设，沿 at₁、at₂ 本身运输两个隶属事实，得到两条前件的满足，假设随后给出公式结论所需的等式。两个方向合起来说明：该公式对单射性是充分的，既不强也不弱。
injAt-in h y x x' p q = h y x x' (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q)
提取一个取值于模型的单射
假设图是单值的且有恰当定义域，定义域的每个元素在图中都有某个像，但那只是仅仅存在的像：定义域隶属给出的是命题截断，而非选定的见证。单值性改变了局面。它表明对一个固定的输入，「一个输出连同该对属于图的证明」构成的类型是命题，而截断的值总能消去到命题中。于是图给出一个真正的、取值在模型中的函数；再假设单射性，便得到真正的单射。这第一层读回把取值保留为载体的元素，是后续证明仍需对编码图作推理时使用的形式。
本节把图 F 与定义域 D 作为模型元素，连同两个满足假设：变元零处图的单值性，以及断言 D 的每个元素在 F 下有取值的恰当定义域条款。环境 γ 按满足判断所期望的固定顺序把它们打包。
module Extract (F D : S) (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩) (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) where γ : S ^ 2 γ = F ∷ D ∷ []
Holds x y 是底层对属于底层图的投影隶属。原像 Fib x 把一个输出 y 与这样的证明配成一对；它的元素就是图在 x 处的候选值，每个候选都带着「它确实是取值」的证书。
Holds : S → S → Type (ℓ-suc ℓ) Holds x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩ Fib : S → Type (ℓ-suc ℓ) Fib x = Σ[ y ∈ S ] Holds x y isPropFib : (x : S) → isProp (Fib x)
要证明 Fib x 是命题，比较 (y,p) 与 (y′,q)。单值性先给出路径 fst y ≡ fst y′。内层 Σ≡Prop 利用 S 元素的第二分量即 isL 证书为命题，把该路径提升为 y ≡ y′；外层 Σ≡Prop 再利用图隶属证明为命题，把这一相等提升为 Fib x 的两个元素相等。这是两个不同的证明无关性步骤，并不是说周遭集合的相等仅由可构造性推出。
isPropFib x (y , p) (y' , q) = Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst F)) (Σ≡Prop (λ z → snd (isL z)) (svAt-out zero γ sv x y y' p q)) toVal : (x : S) → ∥ Fib x ∥₁ → Fib x toVal x = PT.rec (isPropFib x) (λ z → z)
由于 Fib x 是命题，toVal 能把取值的截断存在 ∥ Fib x ∥₁ 消去为实际的原像。选择似乎藏在这里，其实没有：命题截断可以消去到任何命题值的目标，既不需要排中律也不需要选典范代表。定义域 Dom 把输入与其属于 D 的投影证明打包，fib 把由 domAt-in 得到的每个输入的截断像送入 toVal。
Dom : Type (ℓ-suc ℓ) Dom = Σ[ x ∈ S ] ⟨ fst x ∈ fst D ⟩ fib : (u : Dom) → Fib (fst u) fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m) toFun : Dom → S
函数 toFun 把定义域元素送到其唯一原像中的输出 y : S。它只舍去随附的图隶属证明；输出仍是模型元素，因此保留其可构造性证书。定理 toFun-graph 恰把这份被舍去的隶属证据作为原像的第二分量取回。
toFun u = fst (fib u) toFun-graph : (u : Dom) → Holds (fst u) (toFun u) toFun-graph u = snd (fib u) module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where toFun-inj : (u v : Dom) → fst (toFun u) ≡ fst (toFun v)
再假设图的单射性，toFun-inj 把输出的相等变成输入的相等。若 toFun u 与 toFun v 的底层集合相等，就把 u 的图等式沿该路径运输，使两条目都谈及同一个输出即 toFun v；injAt-out 随后比较两个输入，给出 fst u 与 fst v 的第一分量之相等。结论是对投影后的第一分量陈述的，下游基数论证比较 Dom 的元素时用的正是这一形式。
→ fst (fst u) ≡ fst (fst v) toFun-inj u v e = injAt-out zero γ ij (toFun v) (fst u) (fst v) (subst (λ w → ⟨ pr (fst (fst u)) w ∈ fst F ⟩) e (toFun-graph u)) (toFun-graph v)
限制到小载体
函数 toFun 作用在「模型元素连同隶属证明」的对上，这样的载体无法用于基数计数。最后一步把两端都换成典范的小呈现：定义域换成 D 的索引类型，值域换成调用方提供的集合 C 的索引类型，调用方只需证明图的每个取值都落在 C 中。图的三个条款，单值性、恰当定义域与单射性，在此一并假设。呈现层的贡献在于显式性：因为典范嵌入有命题值的原像，属于 D 或 C 都能从索引读出，也能读回索引。
参数点名了起作用的三个可构造集合：图 F、定义域 D 与值域 C。前三个假设正是 Extract 与 toFun-inj 所用的满足陈述。最后一条 ran 是新的：对任意输入 x 与使 (x, y) 属于图的取值 y，它证书化 y 的底层集合属于 C 的底层集合。这是作为调用方假设陈述的取值限制，因此本节本身从不假设图是以某个特定值域造出的。
module Small (F D C : S) (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩) (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) (ij : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩) (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
内层模块以 F、D 与前两个满足证明重新打开 Extract，于是上一节的所有构造都以带前缀的名字可用。接着 toS 把 D 的典范呈现的一个索引 m 变成模型元素。第一分量就是被呈现的集合本身；第二分量是其可构造性证书，由 isL-trans 从显式隶属 member (fst D) m 与 D 自身可构造的证书得出。传递性正是所需的原理：可构造集合的成员是可构造的。
→ ⟨ fst y ∈ fst C ⟩) where module E = Extract F D sv dm toS : ⟪ fst D ⟫ → S toS m = ⟪ fst D ⟫↪ m , isL-trans {x = fst D} {y = ⟪ fst D ⟫↪ m} (member (fst D) m) (snd D)
每个小索引还须被看作 Extract 意义下定义域的成员，at 提供这一对：模型元素 toS m 连同显式隶属证明 member (fst D) m。把 at m 经 E.toFun 喂给图得到一个取值，取值假设证书化该值属于 C。由于典范呈现中的隶属 ⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m)) 是具有命题值原像的嵌入的原像，fiber 返回的是实际的索引 k 连同一条路径，而非仅仅是截断的存在。
at : ⟪ fst D ⟫ → E.Dom at m = toS m , member (fst D) m fib : (m : ⟪ fst D ⟫) → Σ[ k ∈ ⟪ fst C ⟫ ] (⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m))) fib m = fiber (fst C)
舍去路径便得到 small：从 D 的索引类型到 C 的索引类型的函数。每个定义域索引被送到「在图下的像」所对应的索引。至此两种表示会合：small 是固定宇宙层级上类型之间的映射，正是计数论证所需的形状，而它经由保留的路径与图联系在一起。
(ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m))) small : ⟪ fst D ⟫ → ⟪ fst C ⟫ small m = fst (fib m) small-inj : (m n : ⟪ fst D ⟫) → small m ≡ small n → m ≡ n small-inj m n e = ↪-inj {a = fst D} {m = m} {n = n}
small 的单射性由索引的相等沿呈现往返证得。由 small m ≡ small n，反向取 snd (fib m) 得到 m 处的呈现值，嵌入下的同余把相等传过去，snd (fib n) 落到 n 处的呈现值；三条路径按这个确切方向拼接，使两个输出的底层集合相等。Extract 的单射性随之给出两个输入的底层集合相等，而 ↪-inj，即定义域呈现嵌入在索引上的单射性，最终给出 m ≡ n。这里有两个不同的单射性事实在起作用，一个关于图，一个关于典范嵌入，二者不可互相替代。
(E.toFun-inj ij (at m) (at n) (sym (snd (fib m)) ∙ cong ⟪ fst C ⟫↪ e ∙ snd (fib n)))
小结
injAt 在模型内部表达编码图的单射性。单值性与恰当定义域使 Extract.toFun 能把图读成取值于 L 的函数；独立假设 ij 才给出 Extract.toFun-inj。加上指定的值域条件后，Small.small 把该单射转移到定义域和值域的典范小成员类型上。截断步骤使用像原像的唯一性，呈现步骤则使用嵌入原像为命题这一性质。